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

chore: minor optimization

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-11 17:23:59 -08:00
parent 37e63f48cb
commit 017554fbb6
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/type_checker.cpp
View file

@ -675,8 +675,10 @@ bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
bool 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;
expr s_type = infer_type(s);
return is_prop(t_type) && is_def_eq(t_type, s_type);
return is_def_eq(t_type, s_type);
}
bool type_checker::failed_before(expr const & t, expr const & s) const {