From 4ee2f80d66e9f6a507475288c19f11f26c7a889e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Aug 2021 17:33:32 -0700
Subject: [PATCH] fix: improve `binop%` elaborator

---
 src/Lean/Elab/Extra.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 8ed0e1dece..5354aa6ced 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -120,8 +120,12 @@ private structure AnalyzeResult where
   max?            : Option Expr := none
   hasUncomparable : Bool := false -- `true` if there are two types `α` and `β` where we don't have coercions in any direction.
 
-private def isUnknow (e : Expr) : Bool :=
-  e.getAppFn.isMVar
+private def isUnknow : Expr → Bool
+  | Expr.mvar ..        => true
+  | Expr.app f ..       => isUnknow f
+  | Expr.letE _ _ _ b _ => isUnknow b
+  | Expr.mdata _ b _    => isUnknow b
+  | _                   => false
 
 private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM AnalyzeResult := do
   let max? ←