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

fix: do not apply eta for structures in Prop

Browse source 
The eta-expansion contains invalid projections, and the eta-rule is
subsumed by proof irrelevance anyhow.
This commit is contained in:
Gabriel Ebner 2022-03-01 16:34:48 +01:00 • committed by Leonardo de Moura
parent 3746005f5f
commit a7c9d2735f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/inductive.h
View file

@ -67,6 +67,8 @@ inline expr to_cnstr_when_structure(environment const & env, name const & induct
expr e_type = whnf(infer_type(e));
if (!is_constant(get_app_fn(e_type), induct_name))
return e;
if (whnf(infer_type(e_type)) == mk_Prop())
return e;
return expand_eta_struct(env, e_type, e);
}