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

chore: create .toCtorIdx alias only for enumeration types (#10130)

Browse source 
This PR creates the deprecated `.toCtorIdx` alias only for enumeration
types, which are the types that used to have this function. No need
generating an alias for types that never had it. Should reduce the
number of symbols in the standard library.
This commit is contained in:
Joachim Breitner 2025-08-26 10:33:37 +02:00 • committed by GitHub
parent 4f94972ff1
commit aa0cf78d93
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 25 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -79,17 +79,17 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
modifyEnv fun env => addProtected env declName
setReducibleAttribute declName
-- Deprecated alias
-- (Add deprecation attribute after stage0 update)
let aliasName := mkToCtorIdxName indName
addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
(name := aliasName)
(levelParams := info.levelParams)
(type := declType)
(value := mkConst declName us)
(hints := ReducibilityHints.abbrev)
))
modifyEnv fun env => addToCompletionBlackList env aliasName
modifyEnv fun env => addProtected env aliasName
setReducibleAttribute aliasName
Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }
-- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
if (← isEnumType indName) then
let aliasName := mkToCtorIdxName indName
addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
(name := aliasName)
(levelParams := info.levelParams)
(type := declType)
(value := mkConst declName us)
(hints := ReducibilityHints.abbrev)
))
modifyEnv fun env => addToCompletionBlackList env aliasName
modifyEnv fun env => addProtected env aliasName
setReducibleAttribute aliasName
Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }

8
tests/lean/computedFieldsCode.lean.expected.out
View file

@ -26,14 +26,6 @@
let x_2 : tobj := Exp.ctorIdx x_1;
dec x_1;
ret x_2
[Compiler.IR] [result]
def Exp.toCtorIdx (x_1 : @& tobj) : tobj :=
let x_2 : tobj := Exp.ctorIdx x_1;
ret x_2
def Exp.toCtorIdx._boxed (x_1 : tobj) : tobj :=
let x_2 : tobj := Exp.toCtorIdx x_1;
dec x_1;
ret x_2
[Compiler.IR] [result]
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
case x_1 : tobj of

11
tests/lean/run/ctorIdx.lean
View file

@ -69,3 +69,14 @@ inductive Eq' : α → α → Prop where | refl (a : α) : Eq' a a
/-- error: Unknown constant `Eq'.ctorIdx` -/
#guard_msgs in
#print Eq'.ctorIdx
set_option linter.deprecated true
-- Enumeration types get a deprecated alias, other types dont
/-- info: Enum.toCtorIdx : Enum → Nat -/
#guard_msgs in #check Enum.toCtorIdx
/-- warning: `Enum.toCtorIdx` has been deprecated: Use `Enum.ctorIdx` instead -/
#guard_msgs in example := Enum.toCtorIdx
/-- error: Unknown identifier `Nonrec.toCtorIdx` -/
#guard_msgs in #check Nonrec.toCtorIdx