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

chore: revert use of macro_inline for ctorIdx (#10141)

Browse source 
This PR reverts the `macro_inline` part of #10135.
This commit is contained in:
Joachim Breitner 2025-08-26 20:07:49 +02:00 • committed by GitHub
parent 2652cc18b8
commit c83674bdff
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Meta/Constructions/CtorIdx.lean
View file

@ -72,17 +72,13 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
value := mkApp value alt
pure value
mkLambdaFVars (xs.push x) value
let decl := .defnDecl (← mkDefinitionValInferringUnsafe
addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
(name := declName)
(levelParams := info.levelParams)
(type := declType)
(value := declValue)
(hints := ReducibilityHints.abbrev)
)
addDecl decl
if info.numCtors = 1 then
setInlineAttribute declName .macroInline
compileDecl decl
))
modifyEnv fun env => addToCompletionBlackList env declName
modifyEnv fun env => addProtected env declName
setReducibleAttribute declName
@ -90,16 +86,13 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
-- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
if (← isEnumType indName) then
let aliasName := mkToCtorIdxName indName
let decl := .defnDecl (← mkDefinitionValInferringUnsafe
addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
(name := aliasName)
(levelParams := info.levelParams)
(type := declType)
(value := mkConst declName us)
(hints := ReducibilityHints.abbrev)
)
addDecl decl
setInlineAttribute aliasName .macroInline
compileDecl decl
))
modifyEnv fun env => addToCompletionBlackList env aliasName
modifyEnv fun env => addProtected env aliasName
setReducibleAttribute aliasName