From c7c5de38b3cd5dfb4d2b1528b704cd7e2804d3f2 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 8 Jul 2025 10:00:46 -0700 Subject: [PATCH] chore: clean up getDeclNamesForCodeGen (#9259) --- src/Lean/Compiler/Old.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean index aa5b925de8..5d513c7ca9 100644 --- a/src/Lean/Compiler/Old.lean +++ b/src/Lean/Compiler/Old.lean @@ -25,11 +25,11 @@ def isEagerLambdaLiftingName : Name → Bool Here we consider only declarations we generate code for. We use this definition to implement `add_and_compile`. -/ def getDeclNamesForCodeGen : Declaration → Array Name - | Declaration.defnDecl { name := n, .. } => #[n] - | Declaration.mutualDefnDecl defs => defs.toArray.map (·.name) - | Declaration.opaqueDecl { name := n, .. } => #[n] - | Declaration.axiomDecl { name := n, .. } => #[n] -- axiom may be tagged with `@[extern ...]` - | _ => #[] + | .defnDecl { name, .. } => #[name] + | .opaqueDecl { name, .. } => #[name] + | .axiomDecl { name, .. } => #[name] -- axiom may be tagged with `@[extern ...]` + | .mutualDefnDecl defs => defs.toArray.map (·.name) + | _ => #[] def checkIsDefinition (env : Environment) (n : Name) : Except String Unit := do let some info := env.findAsync? n