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

feat(library/equations_compiler/elim_match): do not create auxiliary definition when compiling meta-definitions and/or lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-12 12:54:01 -07:00
parent d980aa3724
commit 2248dccfd4
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1211,6 +1211,10 @@ expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns) {
equations_header header = get_equations_header(eqns);
auto R = elim_match(env, opts, mctx, lctx, eqns);
if (header.m_is_meta || header.m_is_lemma) {
/* Do not generate auxiliary equation or equational lemmas */
return R.m_fn;
}
type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
expr fn_type = ctx1.infer(R.m_fn);
expr fn;