From 2248dccfd4f0446cacb1420d65751038f9bb2e00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Sep 2016 12:54:01 -0700 Subject: [PATCH] feat(library/equations_compiler/elim_match): do not create auxiliary definition when compiling meta-definitions and/or lemmas --- src/library/equations_compiler/elim_match.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index e0380f0e3f..6c3140f67e 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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;