diff --git a/kernel/src/calculus/term.rs b/kernel/src/calculus/term.rs index 07d43c42d2f01dc5154ce0d56029d90c465ba433..5330d334a7a2cf83b1f92a584bd40986ca86eea1 100644 --- a/kernel/src/calculus/term.rs +++ b/kernel/src/calculus/term.rs @@ -314,7 +314,6 @@ mod tests { #[test] fn decl_subst() { use_arena(|arena| { - // λx.(λy.x y) x let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate_with_self( declaration::builder::Builder::Decl(crate::memory::term::builder::Builder::Prop.into(), Vec::new()) .realise(arena) @@ -322,7 +321,6 @@ mod tests { arena, ); let decl = crate::memory::term::Term::decl(decl_, arena); - // λx.x x let reduced = arena.build_term_raw(prop()); assert_eq!(decl.beta_reduction(arena), reduced); diff --git a/kernel/src/memory/level/mod.rs b/kernel/src/memory/level/mod.rs index 51435e1ba0a312630007d02d8d7b0ccfe98f43b5..fdfb7418f16355cef6bf6a0c90cedb9958f53534 100644 --- a/kernel/src/memory/level/mod.rs +++ b/kernel/src/memory/level/mod.rs @@ -226,4 +226,13 @@ mod pretty_printing { ) }) } + + #[test] + fn normalize() { + use_arena(|arena| { + let lvl = arena.build_level_raw(imax(zero(), imax(zero(), imax(succ(zero()), var(0))))); + + assert_eq!(format!("{lvl}"), "max (imax (0) (u0)) (max (imax (0) (u0)) (imax (1) (u0)))") + }) + } }