From 74f137370604bdd80c7ef27a48cab67aa022b105 Mon Sep 17 00:00:00 2001
From: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Date: Wed, 19 Jun 2024 01:44:29 +0200
Subject: [PATCH] chore: remove redundant `if-else` in `isDefEqQuickOther`
 (#4388)

I removed a redundant `if tFn.isMVar || sFn.isMVar then ... else return
LBool.undef` in the `else` clause of
```
if !tFn.isMVar && !sFn.isMVar then
  return LBool.undef
else
```
---
 src/Lean/Meta/ExprDefEq.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index e2a40ca94f..4ac7728295 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1775,15 +1775,12 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         | LBool.true => return LBool.true
         | LBool.false => return LBool.false
         | _ =>
-          if tFn.isMVar || sFn.isMVar then
-            let ctx ← read
-            if ctx.config.isDefEqStuckEx then do
-              trace[Meta.isDefEq.stuck] "{t} =?= {s}"
-              Meta.throwIsDefEqStuck
-            else
-              return LBool.false
+          let ctx ← read
+          if ctx.config.isDefEqStuckEx then do
+            trace[Meta.isDefEq.stuck] "{t} =?= {s}"
+            Meta.throwIsDefEqStuck
           else
-            return LBool.undef
+            return LBool.false
       else
         isDefEqQuickMVarMVar t s