max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: change is_def_eq_proof_irrel type to lbool

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-26 06:59:11 -07:00
parent 8a98987e26
commit 42561bb93f
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/kernel/type_checker.cpp
View file

@ -774,13 +774,13 @@ bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
Return false otherwise. */
bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
lbool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
// Proof irrelevance support for Prop (aka Type.{0})
expr t_type = infer_type(t);
if (!is_prop(t_type))
return false;
return l_undef;
expr s_type = infer_type(s);
return is_def_eq(t_type, s_type);
return to_lbool(is_def_eq(t_type, s_type));
}
bool type_checker::failed_before(expr const & t, expr const & s) const {
@ -938,8 +938,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
if (r != l_undef) return r == l_true;
}
if (is_def_eq_proof_irrel(t_n, s_n))
return true;
r = is_def_eq_proof_irrel(t_n, s_n);
if (r != l_undef) return r == l_true;
r = lazy_delta_reduction(t_n, s_n);
if (r != l_undef) return r == l_true;

2
src/kernel/type_checker.h
View file

@ -81,7 +81,7 @@ private:
lbool try_string_lit_expansion_core(expr const & t, expr const & s);
lbool try_string_lit_expansion(expr const & t, expr const & s);
bool is_def_eq_app(expr const & t, expr const & s);
bool is_def_eq_proof_irrel(expr const & t, expr const & s);
lbool is_def_eq_proof_irrel(expr const & t, expr const & s);
bool failed_before(expr const & t, expr const & s) const;
void cache_failure(expr const & t, expr const & s);
reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);