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

feat: use isProofQuick to implement isDefEqProofIrrel

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-25 08:41:26 -08:00
parent 292603f8bb
commit 856fb0c000
1 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -940,10 +940,19 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
assign t s
private def isDefEqProofIrrel (t s : Expr) : MetaM LBool :=
do tType ← inferType t;
condM (isProp tType)
(do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
(pure LBool.undef)
do status ← isProofQuick t;
match status with
| LBool.false =>
pure LBool.undef
| LBool.true => do
tType ← inferType t;
sType ← inferType s;
toLBoolM $ isExprDefEqAux tType sType
| LBool.undef => do
tType ← inferType t;
condM (isProp tType)
(do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
(pure LBool.undef)
@[inline] def tryL (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool :=
do status ← x;