michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/strategies/rec_strategy): give priority to user defined recursors

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-31 14:54:31 -08:00
parent 76677c4535
commit 4134fdd925
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/nat.lean
View file

@ -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

6
src/library/blast/strategies/rec_strategy.cpp
View file

@ -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<name> 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();
}