inline

leanprover · Nov 8, 2024 · 386f25c · 386f25c
1 parent bf8e2b5
commit 386f25c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 8 deletions.
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
@@ -18,13 +18,6 @@ def DefKind.isTheorem : DefKind → Bool
   | .theorem => true
   | _        => false
 
-def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
-  | .def      => true
-  | .instance => true
-  | .opaque   => true
-  | .abbrev   => true
-  | _         => false
-
 def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
@@ -863,7 +863,7 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
   letRecClosures.foldlM (init := preDefs) fun preDefs c => do
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
-    let kind ← if kind.isDefOrAbbrevOrOpaque then
+    let kind ← if kind matches .def | .instance | .opaque | .abbrev then
       -- Convert any proof let recs inside a `def` to `theorem` kind
       withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind