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

feat(library/blast/recursor_action): ignore type class instances in the recursor action

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-15 18:04:08 -08:00
parent 24ed427c2f
commit 2e057477ef
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/blast/recursor_action.cpp
View file

@ -23,6 +23,11 @@ optional<name> is_recursor_action_target(hypothesis_idx hidx) {
return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc. return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
if (!h->is_assumption()) if (!h->is_assumption())
return optional<name>(); // we only consider assumptions return optional<name>(); // we only consider assumptions
if (get_type_context().is_class(type)) {
// we don't eliminate type classes instances
// TODO(Leo): we may revise that in the future... some type classes instances may be worth eliminating (e.g., decidable).
return optional<name>();
}
// TODO(Leo): more restrictions? // TODO(Leo): more restrictions?
// TODO(Leo): consider user-provided hints // TODO(Leo): consider user-provided hints
expr const & I = get_app_fn(type); expr const & I = get_app_fn(type);