From 87a90c8eb8a63df3ba0d52a0769ff5a2bc3f0b19 Mon Sep 17 00:00:00 2001 From: arthur-adjedj <arthur.adjedj@gmail.com> Date: Thu, 22 Dec 2022 12:44:08 +0100 Subject: [PATCH] chore(kernel): coverage --- kernel/src/calculus/level.rs | 3 +++ kernel/src/memory/term/builder.rs | 1 - 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/kernel/src/calculus/level.rs b/kernel/src/calculus/level.rs index 31c1d3d6..ce4dcb78 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 4887e3fc..9136f581 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)] -- GitLab