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

perf(library/blast/forward/pattern): simplify is_higher_order test

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-02 18:56:48 -08:00
parent a7b3dcbc09
commit 701d6b5016
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/blast/forward/pattern.cpp
View file

@ -192,7 +192,8 @@ namespace blast {
typedef rb_tree<unsigned, unsigned_cmp> idx_metavar_set; typedef rb_tree<unsigned, unsigned_cmp> idx_metavar_set;
static bool is_higher_order(tmp_type_context & ctx, expr const & e) { static bool is_higher_order(tmp_type_context & ctx, expr const & e) {
return is_pi(ctx.relaxed_whnf(ctx.infer(e))); /* Remark: it is too expensive to use ctx.relaxed_whnf here. */
return is_pi(ctx.whnf(ctx.infer(e)));
} }
/** \brief Given type of the form (Pi (a_1 : A_1) ... (a_n : A_n), B) (or reducible to something of this form), /** \brief Given type of the form (Pi (a_1 : A_1) ... (a_n : A_n), B) (or reducible to something of this form),