From 1a36ebe144d1231b3698ce18f48b0da574b71111 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 d9882178..86417519 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -349,4 +349,17 @@ mod tests {
.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())));
+ 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())
+ }
}
--
GitLab