From e8b58abdb2702aecdc7b058cac3afd767483afff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Jul 2022 07:47:28 -0400
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Meta/ExprDefEq.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 3684d04217..1533a1f9f9 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1333,15 +1333,6 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   if tArgs.size < fvars.size then return none
   return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
 
-private def isSynthetic : Expr → MetaM Bool
-  | Expr.mvar mvarId => do
-    let mvarDecl ← getMVarDecl mvarId
-    match mvarDecl.kind with
-    | MetavarKind.synthetic       => pure true
-    | MetavarKind.syntheticOpaque => pure true
-    | MetavarKind.natural         => pure false
-  | _                  => pure false
-
 private def isAssignable : Expr → MetaM Bool
   | Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
   | _                => pure false