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

fix(frontends/lean/elaborator): get_elim_info_for_builtin

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-13 14:17:08 -07:00
parent 9765151156
commit cf1c50f4e9
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/elaborator.cpp
View file

@ -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)) {

4
tests/lean/run/new_elab2.lean Normal file
View file

@ -0,0 +1,4 @@
set_option new_elaborator true
theorem ex {a : Prop} (H : ¬a) : a ↔ false :=
iff.intro H (false.rec a)