max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: clean up getDeclNamesForCodeGen (#9259)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-08 10:00:46 -07:00 • committed by GitHub
parent 6ad12525ad
commit c7c5de38b3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Compiler/Old.lean
View file

@ -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