diff --git a/library/init/nat.lean b/library/init/nat.lean index 0f30a6f7a..cc91249ad 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -22,6 +22,8 @@ namespace nat {C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C (succ a)) : C n := nat.rec H₁ (λ a ih, H₂ a) n + attribute nat.rec_on [recursor] -- Hack: force rec_on to be the first one. TODO(Leo): we should add priorities to recursors + protected definition no_confusion_type [reducible] (P : Type) (v₁ v₂ : ℕ) : Type := nat.rec (nat.rec diff --git a/src/library/blast/strategies/rec_strategy.cpp b/src/library/blast/strategies/rec_strategy.cpp index 54e84dc7c..398731bc3 100644 --- a/src/library/blast/strategies/rec_strategy.cpp +++ b/src/library/blast/strategies/rec_strategy.cpp @@ -22,13 +22,13 @@ static action_result try_hypothesis(hypothesis_idx hidx) { expr const & I = get_app_fn(type); lean_assert(is_constant(I)); name const & I_name = const_name(I); - if (inductive::is_inductive_decl(env(), I_name)) { - return recursor_action(hidx, inductive::get_elim_name(I_name)); - } list Rs = get_recursors_for(env(), const_name(I)); if (Rs) { return recursor_action(hidx, head(Rs)); } + if (inductive::is_inductive_decl(env(), I_name)) { + return recursor_action(hidx, inductive::get_elim_name(I_name)); + } return action_result::failed(); }