From 49323ab598e85622d8e05127a481b5ed113e6872 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 13:44:55 -0800 Subject: [PATCH] feat(library/util): add mk_symm --- src/library/util.cpp | 10 ++++++++++ src/library/util.h | 1 + 2 files changed, 11 insertions(+) diff --git a/src/library/util.cpp b/src/library/util.cpp index 8121aeaaf..ac0af5976 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -324,6 +324,16 @@ expr mk_refl(type_checker & tc, expr const & a) { return mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a); } +expr mk_symm(type_checker & tc, expr const & H) { + expr p = tc.whnf(tc.infer(H).first).first; + lean_assert(is_eq(p)); + expr lhs = app_arg(app_fn(p)); + expr rhs = app_arg(p); + expr A = tc.infer(lhs).first; + level lvl = sort_level(tc.ensure_type(A).first); + return mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H); +} + expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) { expr A = tc.whnf(tc.infer(lhs).first).first; expr B = tc.whnf(tc.infer(rhs).first).first; diff --git a/src/library/util.h b/src/library/util.h index 891f539bb..6b714da41 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -114,6 +114,7 @@ expr mk_pr2(type_checker & tc, expr const & p, bool prop); expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs); expr mk_refl(type_checker & tc, expr const & a); +expr mk_symm(type_checker & tc, expr const & H); bool is_eq_rec(expr const & e); bool is_eq(expr const & e); /** \brief Return true iff \c e is of the form (eq A a a) */