chore: remove syntax for extern arity specifications (#9556)

src/Lean/Compiler/ExternAttr.lean

@@ -36,8 +36,6 @@ inductive ExternEntry where
    encoding: ```.entries = [inline `cpp "#1 + #2"]```
 - `@[extern cpp "foo" llvm adhoc]`
    encoding: ```.entries = [standard `cpp "foo", adhoc `llvm]```
-- `@[extern 2 cpp "io_prim_println"]`
-   encoding: ```.arity? = 2, .entries = [standard `cpp "ioPrimPrintln"]```
 -/
 structure ExternAttrData where
   entries  : List ExternEntry
@@ -46,7 +44,7 @@ structure ExternAttrData where
 -- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit
 -- @[builtin_attr_parser] def extern     := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry
 private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
-  let entriesStx := stx[2].getArgs
+  let entriesStx := stx[1].getArgs
   if entriesStx.size == 0 then
     return { entries := [ ExternEntry.adhoc `all ] }
   let mut entries := #[]

src/Lean/Environment.lean

@@ -1829,9 +1829,9 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
   When we a new user-defined attribute declaration is imported, `attributeMapRef` is updated.
   Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
-@[extern 2 "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment
+@[extern "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment
 /-- "Forward declaration" for retrieving the number of builtin attributes. -/
-@[extern 1 "lean_get_num_attributes"] opaque getNumBuiltinAttributes : IO Nat
+@[extern "lean_get_num_attributes"] opaque getNumBuiltinAttributes : IO Nat
 
 private def ensureExtensionsArraySize (env : Environment) : IO Environment := do
   let exts ← EnvExtension.ensureExtensionsArraySize env.base.private.extensions

src/Lean/Meta/Basic.lean

@@ -744,7 +744,7 @@ The result may contain subexpressions that have not been reduced.
 
 See `Lean.Meta.whnfImp` for the implementation.
 -/
-@[extern 6 "lean_whnf"] opaque whnf : Expr → MetaM Expr
+@[extern "lean_whnf"] opaque whnf : Expr → MetaM Expr
 /--
 Returns the inferred type of the given expression. Assumes the expression is type-correct.
 
@@ -798,10 +798,10 @@ def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
 
 See `Lean.Meta.inferTypeImp` for the implementation of `inferType`.
 -/
-@[extern 6 "lean_infer_type"] opaque inferType : Expr → MetaM Expr
-@[extern 7 "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
-@[extern 7 "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool
-@[extern 6 "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool
+@[extern "lean_infer_type"] opaque inferType : Expr → MetaM Expr
+@[extern "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
+@[extern "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool
+@[extern "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool
 
 def whnfForall (e : Expr) : MetaM Expr := do
   let e' ← whnf e

src/Lean/Parser/Attr.lean

@@ -52,7 +52,7 @@ namespace Attr
 def externEntry := leading_parser
   optional (ident >> ppSpace) >> optional (nonReservedSymbol "inline ") >> strLit
 @[builtin_attr_parser] def extern     := leading_parser
-  nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
+  nonReservedSymbol "extern" >> many (ppSpace >> externEntry)
 
 /--
 Declare this tactic to be an alias or alternative form of an existing tactic.

tests/lean/run/extern.lean

@@ -4,9 +4,6 @@ def foo (x : Nat) := x
 @[extern "bla"]
 def foo2 (x : Nat) := x
 
-@[extern 2 "boo"]
-def foo3 (x : Nat) := x
-
 @[extern cpp "Lean::bla" llvm "lean_bla"]
 def foo4 (x : Bool) := x