From a7c9d2735f68cafcf4dca5debe665cd2c1f1771f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 1 Mar 2022 16:34:48 +0100 Subject: [PATCH] fix: do not apply eta for structures in Prop The eta-expansion contains invalid projections, and the eta-rule is subsumed by proof irrelevance anyhow. --- src/kernel/inductive.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h index 27feac701d..dd6b2671b2 100644 --- a/src/kernel/inductive.h +++ b/src/kernel/inductive.h @@ -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); }