max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-12 19:55:26 -07:00
parent 96d00ff2d7
commit 04ecce0085
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/library/compiler/csimp.cpp generated
View file

@ -1149,7 +1149,8 @@ class csimp_fn {
// Example: `fun {a} => ReaderT.pure`
if (!is_join_point_def && !top) {
expr new_e = eta_reduce(e);
if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
// Remark: we should not eta-reduce auxiliary match applications.
if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_matcher_app(env(), new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
return visit(new_e, true);
}
buffer<expr> binding_fvars;

5
stage0/src/library/compiler/util.h generated
View file

@ -204,6 +204,11 @@ inline bool is_matcher(environment const & env, name const & n) {
return lean_is_matcher(env.to_obj_arg(), n.to_obj_arg());
}
inline bool is_matcher_app(environment const & env, expr const & e) {
expr const & f = get_app_fn(e);
return is_constant(f) && is_matcher(env, const_name(f));
}
void initialize_compiler_util();
void finalize_compiler_util();
}