From 674278f5614fcdb835b1750376563f5ed435cc7d Mon Sep 17 00:00:00 2001
From: v-lafeychine <vincent.lafeychine@proton.me>
Date: Thu, 27 Oct 2022 15:49:35 +0200
Subject: [PATCH] =?UTF-8?q?Resolve=20"proost=20fonctionality=20and=20UI"?=
=?UTF-8?q?=20=E2=9C=A8=EF=B8=8F=20Closes=20#22=20et=20#7=20=F0=9F=90=94?=
=?UTF-8?q?=EF=B8=8F=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20aalbert=20<augu?=
=?UTF-8?q?stin.albert@bleu-azure.fr>=20Approved-by:=20belazy=20<aarthuur0?=
=?UTF-8?q?1@gmail.com>=20Approved-by:=20loutr=20<loutr@crans.org>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* Chore : add test
* Fix : shift vars when binding lambda-abstractions
* fix(kernel): some tests were wrong
* HOT fix(kernel): command definition fixed
* HOT fix(parser): fix parenthesis
* HOT fix(parser): order of fun
* feat(parser): resolve threads
* chore(parser): Merge renamed_rules on Error
* chore(command): Merge Define/DefineCheckType + Add tests
* chore(parser): apply suggestions
* feat(parser): add location conversion from pest to proost's kernel
* Apply 1 suggestion(s) to 1 file(s)
* fix(all): resolve thread and change Pos for Loc (range position) +
conversion from position to range position in parser
* fix(all): resolve threads
* feat(kernel): Add tests in commands.rs
* feat(parser, error): add new errors for parser, pos struct, first use of pos and pretty print of parsing errors
* feat(parser, kernel): new kernel error: cannot parse
* feat(proost): new ui v1
* feat(proost): new interface!
* feat(parser, kernel): change grammar and pretty printing
---
kernel/src/type_checker.rs | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 043060dc..b879f5b5 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -424,4 +424,24 @@ mod tests {
);
assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
}
+
+ #[test]
+ fn prod_var() {
+ let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
+ let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ assert!(t.check(&ty, &Environment::new()).is_ok())
+ }
+
+ #[test]
+ fn univ_reduc() {
+ let ty = App(
+ box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
+ box Prod(box Prop, box Var(1.into())),
+ );
+ assert!(ty.conversion(
+ &Type(BigUint::from(0_u64).into()),
+ &Environment::new(),
+ 0.into()
+ ))
+ }
}
--
GitLab