From 269fb198fbcfcf8d1314496bcaa3aefb08727beb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Oct 2016 23:34:14 -0700 Subject: [PATCH] perf(library/type_context): process function before arguments --- src/library/type_context.cpp | 4 ++-- tests/lean/run/simplifier_canonize_subsingletons.lean | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 81b20eefbd..c409a91c45 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2456,8 +2456,8 @@ bool type_context::is_def_eq_core_core(expr const & t, expr const & s) { if (is_app(t_n) && is_app(s_n)) { scope s(*this); - if (is_def_eq_args(t_n, s_n) && - is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) && + if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) && + is_def_eq_args(t_n, s_n) && process_postponed(s)) { s.commit(); return true; diff --git a/tests/lean/run/simplifier_canonize_subsingletons.lean b/tests/lean/run/simplifier_canonize_subsingletons.lean index 326f0ce784..4801485644 100644 --- a/tests/lean/run/simplifier_canonize_subsingletons.lean +++ b/tests/lean/run/simplifier_canonize_subsingletons.lean @@ -60,9 +60,9 @@ end lambda namespace dont_crash_when_locals_incompatible -universe variable l +universe variables l constants (ss : Π {A : Type.{l}}, A → Type.{l}) - [ss_ss : ∀ (T : Type*) (t : T), subsingleton (ss t)] + [ss_ss : ∀ (T : Type l) (t : T), subsingleton (ss t)] (A : Type.{l}) (a : A) (ss₁ ss₂ : ss a) @@ -77,7 +77,7 @@ example : (λ (s : ss a), ss₁) = (λ (s : ss a), s) := by simp -- first. We do however avoid the error of replacing ss₁ with the local s. -- TODO(dhs): the more robust solution is to maintain a set of canonical (_ : ss a) -- for each subsingleton type, analogous to the defeq_canonizer. -example : (λ (s : ss a), s) = (λ (s : ss a), ss₁) := +lemma ex : (λ (s : ss a.{1}), s) = (λ (s : ss a.{1}), ss₁) := by do try simp, f ← mk_const `funext, apply f,