From 10f4a22fffcac3873c5b4e5ab07732e5fdb2cbea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Sep 2016 11:14:49 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): try to synthesize pending type class instances before processing eliminator/recursor --- src/frontends/lean/elaborator.cpp | 2 +- tests/lean/run/div_wf.lean | 11 +++++++---- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a897a1e7d5..b0fd05a812 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -717,7 +717,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< format("(it is handled as an \"eliminator\"), ") + format("but the expected type must be known")); } - + synthesize_type_class_instances(); expr expected_type = instantiate_mvars(*_expected_type); if (has_expr_metavar(expected_type)) { auto pp_fn = mk_pp_ctx(); diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean index cadba11cda..b2629e9cfa 100644 --- a/tests/lean/run/div_wf.lean +++ b/tests/lean/run/div_wf.lean @@ -1,17 +1,20 @@ +set_option new_elaborator true open nat well_founded decidable prod +set_option pp.all true + -- Auxiliary lemma used to justify recursive call private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x := and.rec_on H (λ ypos ylex, sub_lt (nat.lt_of_lt_of_le ypos ylex) ypos) definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := -if H : 0 < y ∧ y ≤ x then f (x - y) (lt_aux H) y + 1 else zero +if H : 0 < y ∧ y ≤ x then f (x - y) (lt_aux H) y + 1 else 0 definition wdiv (x y : nat) := fix lt_wf wdiv.F x y -theorem wdiv_def (x y : nat) : wdiv x y = if 0 < y ∧ y ≤ x then wdiv (x - y) y + 1 else 0 := +theorem wdiv_def (x y : nat) : wdiv x y = if H : 0 < y ∧ y ≤ x then wdiv (x - y) y + 1 else 0 := congr_fun (well_founded.fix_eq lt_wf wdiv.F x) y example : wdiv 5 2 = 2 := @@ -36,12 +39,12 @@ lex.left _ _ _ (lt_aux H) definition pdiv.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat := prod.cases_on p₁ (λ x y f, - if H : 0 < y ∧ y ≤ x then f (x - y, y) (plt_aux x y H) + 1 else zero) + if H : 0 < y ∧ y ≤ x then f (x - y, y) (plt_aux x y H) + 1 else 0) definition pdiv (x y : nat) := fix pair_nat.lt.wf pdiv.F (x, y) -theorem pdiv_def (x y : nat) : pdiv x y = if 0 < y ∧ y ≤ x then pdiv (x - y) y + 1 else zero := +theorem pdiv_def (x y : nat) : pdiv x y = if H : 0 < y ∧ y ≤ x then pdiv (x - y) y + 1 else 0 := well_founded.fix_eq pair_nat.lt.wf pdiv.F (x, y) example : pdiv 17 2 = 8 :=