michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/util): add mk_refl

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-18 18:23:59 -08:00
parent a97bef7df2
commit 9bd74689be
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/util.cpp
View file

@ -299,6 +299,12 @@ expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs); return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs);
} }
expr mk_refl(type_checker & tc, expr const & a) {
expr A = tc.whnf(tc.infer(a).first).first;
level lvl = sort_level(tc.ensure_type(A).first);
return mk_app(mk_constant(*g_eq_refl_name, {lvl}), A, a);
}
expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) { expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) {
expr A = tc.whnf(tc.infer(lhs).first).first; expr A = tc.whnf(tc.infer(lhs).first).first;
expr B = tc.whnf(tc.infer(rhs).first).first; expr B = tc.whnf(tc.infer(rhs).first).first;

1
src/library/util.h
View file

@ -90,6 +90,7 @@ expr mk_pr1(type_checker & tc, expr const & p, bool prop);
expr mk_pr2(type_checker & tc, expr const & p, bool prop); 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_eq(type_checker & tc, expr const & lhs, expr const & rhs);
expr mk_refl(type_checker & tc, expr const & a);
/** \brief Create a telescope equality for HoTT library. /** \brief Create a telescope equality for HoTT library.
This procedure assumes eq supports dependent elimination. This procedure assumes eq supports dependent elimination.