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

feat(library/util): add mk_symm

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-04 13:44:55 -08:00
parent ccae014ef9
commit 49323ab598
2 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/util.cpp
View file

@ -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); 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 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

@ -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_eq(type_checker & tc, expr const & lhs, expr const & rhs);
expr mk_refl(type_checker & tc, expr const & a); 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_rec(expr const & e);
bool is_eq(expr const & e); bool is_eq(expr const & e);
/** \brief Return true iff \c e is of the form (eq A a a) */ /** \brief Return true iff \c e is of the form (eq A a a) */