From 0afcb8bc9f7d0569b6bcb8baebfdce82788c02a7 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 15:07:56 +0100
Subject: [PATCH] Fix : century-old bug in the type-checker
---
kernel/src/term.rs | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index f12f1ad4..efa321a0 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -337,6 +337,19 @@ mod tests {
}
+ #[test]
+ fn poly_univ_id(){
+ let id_ty = Prod(box Type(UniverseLevel::Var(0)),box Prod(box Var(1.into()),box Var(2.into())));
+ let id_te = Abs(box Type(UniverseLevel::Var(0)),box Abs(box Var(1.into()),box Var(1.into())));
+ let id_zero = Abs(box Type(0.into()),box Abs(box Var(1.into()),box Var(1.into())));
+ assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
+ let env = Environment::new()
+ .insert("id".into(), id_te.clone().into(), id_ty.clone())
+ .unwrap();
+ assert!(Const("id".into(),vec![0.into()]).is_def_eq(&id_zero, &env).is_ok())
+ }
+
+
#[test]
fn poly_univ_id(){
let id_ty = Prod(box Type(UniverseLevel::Var(0)),box Prod(box Var(1.into()),box Var(2.into())));
--
GitLab