From cf1c50f4e9ce4732ac535c8f0277a80b18e0e013 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Sep 2016 14:17:08 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): get_elim_info_for_builtin --- src/frontends/lean/elaborator.cpp | 5 +++++ tests/lean/run/new_elab2.lean | 4 ++++ 2 files changed, 9 insertions(+) create mode 100644 tests/lean/run/new_elab2.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d108f41b2c..3937c21ba3 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -269,6 +269,11 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info { r.m_arity = nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors; } r.m_nexplicit = 1 /* major premise */ + nminors; + if (nminors == 0) { + /* The motive is marked as explicit in builtin recursors that do not have + minor premises */ + r.m_nexplicit++; + } r.m_motive_idx = nparams; unsigned major_idx; if (inductive::is_elim_rule(m_env, fn)) { diff --git a/tests/lean/run/new_elab2.lean b/tests/lean/run/new_elab2.lean new file mode 100644 index 0000000000..c5f94b3671 --- /dev/null +++ b/tests/lean/run/new_elab2.lean @@ -0,0 +1,4 @@ +set_option new_elaborator true + +theorem ex {a : Prop} (H : ¬a) : a ↔ false := +iff.intro H (false.rec a)