From 6e6f778ecfdc6c8c83d9185bd2353c7ea80c72a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 12:57:25 -0700 Subject: [PATCH] fix(kernel/converter): missing case for local constants Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 4 ++-- src/kernel/converter.cpp | 4 ++++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 7256eb882..9f9dfcdf7 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -86,8 +86,8 @@ definition cast {A B : Type} (H : A = B) (a : A) : B := eq_rec a H -- TODO(Leo): check why unifier needs 'help' in the following theorem -theorem cast_refl.{l} {A : Type.{l}} (a : A) : @cast.{l} A A (refl A) a = a -:= refl (@cast.{l} A A (refl A) a) +theorem cast_refl.{l} {A : Type.{l}} (a : A) : cast (refl A) a = a +:= refl (cast (refl A) a) definition iff (a b : Bool) := (a → b) ∧ (b → a) infix `↔` 50 := iff diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 5bd8880b9..c23caf7d9 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -415,6 +415,10 @@ struct default_converter : public converter { is_def_eq(const_levels(t_n), const_levels(s_n), c, jst)) return true; + if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n) && + is_def_eq(mlocal_type(t_n), mlocal_type(s_n), c, jst)) + return true; + // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance) if (is_app(t_n) && is_app(s_n)) { type_checker::scope scope(c);