From 4e33ca472dcd74b0ac0c9a0e8143ee76a1797d52 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Aug 2016 15:12:19 -0700 Subject: [PATCH] feat(library/tactic/defeq_simplifier): add helper function --- src/library/tactic/defeq_simplifier/defeq_simplifier.cpp | 5 +++++ src/library/tactic/defeq_simplifier/defeq_simplifier.h | 1 + 2 files changed, 6 insertions(+) diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp b/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp index 0b020314e1..882387ea63 100644 --- a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp +++ b/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp @@ -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); diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.h b/src/library/tactic/defeq_simplifier/defeq_simplifier.h index 86121c641c..ee69dd15b6 100644 --- a/src/library/tactic/defeq_simplifier/defeq_simplifier.h +++ b/src/library/tactic/defeq_simplifier/defeq_simplifier.h @@ -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(); }