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

chore(library/equations_compiler): test elim_match on nonrec equations

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-18 21:00:57 -07:00
parent 50c147cd0e
commit 06b02e4912
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -29,6 +29,8 @@ expr compile_equations(environment & env, options const & opts, metavar_context
optional<expr> eqns1 = try_structural_rec(ctx.get(), eqns, arg_idx);
if (eqns1) {
elim_match(env, opts, mctx, lctx, *eqns1);
} else if (!is_recursive_eqns(ctx, eqns)) {
elim_match(env, opts, mctx, lctx, eqns);
}
// test unbounded_rec