michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/definitional/equations): bug in "complete" transition

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-05 16:27:29 -08:00
parent 3889b60152
commit eedc31f7e9
2 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/definitional/equations.cpp
View file

@ -834,7 +834,7 @@ class equation_compiler_fn {
expr c = mk_constructor(c_name, I_ls, I_params, new_args);
list<expr> new_ctx = to_list(new_args.begin(), new_args.end(), rest_ctx);
list<expr> new_patterns = cons(c, tail(e.m_patterns));
new_eqns.push_back(eqn(e, new_ctx, new_patterns));
new_eqns.push_back(replace(eqn(e, new_ctx, new_patterns), p, c));
}
} else {
new_eqns.push_back(e);

5
tests/lean/run/eq17.lean Normal file
View file

@ -0,0 +1,5 @@
open nat
definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b,
lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a)),
lt_of_succ (lt.step h) := lt.step (lt_of_succ h)