diff --git a/kernel/src/calculus/level.rs b/kernel/src/calculus/level.rs index 31c1d3d608b3b4b24ba4ed6adb2c451ee54deeaf..ce4dcb78e992cbc0d670ca6d7da0a5d8099187ba 100644 --- a/kernel/src/calculus/level.rs +++ b/kernel/src/calculus/level.rs @@ -94,6 +94,8 @@ mod tests { let zero_ = arena.build_level_raw(zero()); let var0 = Level::var(0, arena); let var1 = Level::var(1, arena); + let succ_var0 = Level::succ(var0,arena); + let max1_var0 = Level::max(one, var0, arena); let max0_var0 = Level::max(zero_, var0, arena); let max_var0_var1 = Level::max(var0, var1, arena); let max_var1_var0 = Level::max(var1, var0, arena); @@ -101,6 +103,7 @@ mod tests { let succ_max_var0_var1 = Level::succ(max_var0_var1, arena); let max_succ_var0_succ_var1 = arena.build_level_raw(max(succ(var(0)), succ(var(1)))); + assert!(max1_var0.geq(succ_var0,0,arena)); assert!(!zero_.is_eq(one, arena)); assert!(!one.is_eq(zero_, arena)); assert!(var0.is_eq(max0_var0, arena)); diff --git a/kernel/src/memory/term/builder.rs b/kernel/src/memory/term/builder.rs index 4887e3fc88d4b2eb51bf440a7d2b8c4fb176e33e..9136f581b6059c8ae1e32a27dcb87ef95ebcdafc 100644 --- a/kernel/src/memory/term/builder.rs +++ b/kernel/src/memory/term/builder.rs @@ -21,7 +21,6 @@ use crate::error::{Error, ResultTerm}; use crate::memory::arena::Arena; use crate::memory::declaration::builder as declaration; use crate::memory::level::builder as level; -use crate::error::{Error, ResultTerm}; #[non_exhaustive] #[derive(Clone, Debug, Display, Eq, PartialEq)]