diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs index 2b574a8329e57d7011dd7cf5d851381b958cee74..e577d8a426a5921c0eee279fcd04049c5187e083 100644 --- a/kernel/src/type_checker.rs +++ b/kernel/src/type_checker.rs @@ -48,11 +48,11 @@ impl<'arena> Arena<'arena> { fn conversion(&mut self, lhs: Term<'arena>, rhs: Term<'arena>) -> bool { lhs == rhs || match (&*self.whnf(lhs), &*self.whnf(rhs)) { - (&Prop, &Prop) => true, + (Prop, Prop) => true, - (&Type(ref i), &Type(ref j)) => i == j, + (Type(i), Type(j)) => *i == *j, - (&Var(i, _), &Var(j, _)) => i == j, + (Var(i, _), Var(j, _)) => i == j, (&Prod(t1, u1), &Prod(t2, u2)) => { self.conversion(t1, t2) && self.conversion(u1, u2)