From a97bef7df20270697c705118a8b82b20bd51800e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Dec 2014 15:53:23 -0800 Subject: [PATCH] feat(library/util): add mk_heq --- src/library/util.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/library/util.cpp b/src/library/util.cpp index d3feb7ed4..9c4c6d5eb 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -171,6 +171,8 @@ static name * g_eq_name = nullptr; static name * g_eq_refl_name = nullptr; static name * g_eq_rec_name = nullptr; +static name * g_heq_name = nullptr; + static name * g_sigma_name = nullptr; static name * g_sigma_mk_name = nullptr; @@ -193,6 +195,8 @@ void initialize_library_util() { g_eq_refl_name = new name{"eq", "refl"}; g_eq_rec_name = new name{"eq", "rec"}; + g_heq_name = new name("heq"); + g_sigma_name = new name("sigma"); g_sigma_mk_name = new name{"sigma", "dpair"}; } @@ -213,6 +217,7 @@ void finalize_library_util() { delete g_eq_name; delete g_eq_refl_name; delete g_eq_rec_name; + delete g_heq_name; delete g_sigma_name; delete g_sigma_mk_name; } @@ -294,6 +299,13 @@ expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) { return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs); } +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; + level lvl = sort_level(tc.ensure_type(A).first); + return mk_app(mk_constant(*g_heq_name, {lvl}), A, lhs, B, rhs); +} + void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer const & s, buffer & eqs) { lean_assert(t.size() == s.size()); lean_assert(std::all_of(s.begin(), s.end(), is_local));