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

feat(library/tactic/defeq_simplifier): add helper function

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-31 15:12:19 -07:00
parent 51a338d9a1
commit 4e33ca472d
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
View file

@ -350,6 +350,11 @@ vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0)
LEAN_TACTIC_CATCH(s);
}
expr defeq_simplify(type_context & ctx, expr const & e) {
defeq_simp_lemmas lemmas = get_defeq_simp_lemmas(ctx.env());
return defeq_simplify(ctx, lemmas, e);
}
/* Setup and teardown */
void initialize_defeq_simplifier() {
DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp_core"}), tactic_defeq_simp);

1
src/library/tactic/defeq_simplifier/defeq_simplifier.h
View file

@ -10,6 +10,7 @@ Author: Daniel Selsam
namespace lean {
expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e);
expr defeq_simplify(type_context & ctx, expr const & e);
void initialize_defeq_simplifier();
void finalize_defeq_simplifier();
}