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

fix(library/equations_compiler/elim_match): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-02 12:39:21 -07:00
parent 3e4d8d0f75
commit b3d78208be
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/equations_compiler/elim_match.cpp
View file

@ -644,7 +644,7 @@ struct elim_match_fn {
expr new_arg = ctx.push_local(binding_name(it), binding_domain(it));
new_args.push_back(new_arg);
c = mk_app(c, new_arg);
it = whnf_inductive(ctx, instantiate(binding_body(new_arg), new_arg));
it = whnf_inductive(ctx, instantiate(binding_body(it), new_arg));
}
if (ctx.is_def_eq(pattern_type, it)) {
equation new_eqn = eqn;