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-21 09:23:04 -08:00
parent aa7afb7285
commit 64907481d7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/Init/Lean/Meta/ExprDefEq.lean
View file

@ -811,8 +811,8 @@ do decl ← getLocalDecl fvarId;
private partial def isDefEqQuick : Expr → Expr → MetaM LBool
| Expr.lit l₁ _, Expr.lit l₂ _ => pure (l₁ == l₂).toLBool
| Expr.sort u _, Expr.sort v _ => toLBoolM $ isLevelDefEqAux u v
| t@(Expr.lam _ _ _ _), s@(Expr.lam _ _ _ _) => toLBoolM $ isDefEqBinding t s
| t@(Expr.forallE _ _ _ _), s@(Expr.forallE _ _ _ _) => toLBoolM $ isDefEqBinding t s
| t@(Expr.lam _ _ _ _), s@(Expr.lam _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s
| t@(Expr.forallE _ _ _ _), s@(Expr.forallE _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s
| Expr.mdata _ t _, s => isDefEqQuick t s
| t, Expr.mdata _ s _ => isDefEqQuick t s
| Expr.fvar fvarId₁ _, Expr.fvar fvarId₂ _ =>