From 017554fbb6c472cb1ef806977c2b52c9630f577c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Nov 2019 17:23:59 -0800 Subject: [PATCH] chore: minor optimization --- src/kernel/type_checker.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 50ab706531..cd12c265b3 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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 {