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

refactor(library/util): rename old is_eq_rec

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-06 16:51:16 -08:00
parent 2482c49729
commit 34d5882b9a
3 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/inversion_tactic.cpp
View file

@ -552,7 +552,7 @@ class inversion_tac {
expr const & eq = binding_domain(type); expr const & eq = binding_domain(type);
expr const & lhs = app_arg(app_fn(eq)); expr const & lhs = app_arg(app_fn(eq));
expr const & rhs = app_arg(eq); expr const & rhs = app_arg(eq);
lean_assert(is_eq_rec(lhs)); lean_assert(is_eq_rec_core(lhs));
// lhs is of the form (eq.rec A s C a s p) // lhs is of the form (eq.rec A s C a s p)
// aux_eq is a term of type ((eq.rec A s C a s p) = a) // aux_eq is a term of type ((eq.rec A s C a s p) = a)
auto aux_eq = apply_eq_rec_eq(m_tc, m_ios, to_list(hyps), lhs); auto aux_eq = apply_eq_rec_eq(m_tc, m_ios, to_list(hyps), lhs);
@ -656,7 +656,7 @@ class inversion_tac {
eq = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs); eq = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs);
type = update_binding(type, eq, binding_body(type)); type = update_binding(type, eq, binding_body(type));
} }
if (!m_proof_irrel && is_eq_rec(new_lhs)) { if (!m_proof_irrel && is_eq_rec_core(new_lhs)) {
return intro_next_eq_rec(g, type); return intro_next_eq_rec(g, type);
} else { } else {
return intro_next_eq_simple(g, type); return intro_next_eq_simple(g, type);

2
src/library/util.cpp
View file

@ -575,7 +575,7 @@ expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) {
return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs); return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs);
} }
bool is_eq_rec(expr const & e) { bool is_eq_rec_core(expr const & e) {
expr const & fn = get_app_fn(e); expr const & fn = get_app_fn(e);
return is_constant(fn) && const_name(fn) == get_eq_rec_name(); return is_constant(fn) && const_name(fn) == get_eq_rec_name();
} }

5
src/library/util.h
View file

@ -159,7 +159,10 @@ expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const
expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h); expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h);
/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_hprop.elim (in HoTT mode) */ /** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_hprop.elim (in HoTT mode) */
expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y); expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y);
bool is_eq_rec(expr const & e);
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
bool is_eq_rec_core(expr const & e);
bool is_eq(expr const & e); bool is_eq(expr const & e);
bool is_eq(expr const & e, expr & lhs, expr & rhs); bool is_eq(expr const & e, expr & lhs, expr & rhs);
/** \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) */