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) */