fix: check that funind-reserved names are available

src/Lean/Elab/PreDefinition/Main.lean

@@ -90,6 +90,11 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
+def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM Unit := do
+  preDefs.forM fun preDef =>
+    withRef preDef.ref <| ensureReservedNameAvailable preDef.declName "induct"
+  withRef preDefs[0]!.ref <| ensureReservedNameAvailable preDefs[0]!.declName "mutual_induct"
+
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -121,6 +126,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       addAndCompilePartial preDefs
       preDefs.forM (·.termination.ensureNone "partial")
     else
+      ensureFunIndReservedNamesAvailable preDefs
       try
         let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then

tests/lean/funind_reserved.lean

@@ -0,0 +1,96 @@
+
+-- Test that the reserved name availability is checked at function definition time
+
+namespace Nonrec
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- no error (yet)
+  | 0 => 0
+  | n+1 => n
+
+end Nonrec
+
+namespace Structural
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+
+end Structural
+
+namespace WF
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+
+end WF
+
+namespace Mutual1
+
+def foo.induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual1
+
+namespace Mutual2
+
+def bar.induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual2
+
+namespace Mutual3
+
+def foo.mutual_induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual3
+
+namespace Nested
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+  where induct := 1
+
+end Nested

tests/lean/funind_reserved.lean.expected.out

@@ -0,0 +1,6 @@
+funind_reserved.lean:18:4-18:7: error: failed to declare `Structural.foo` because `Structural.foo.induct` has already been declared
+funind_reserved.lean:28:4-28:7: error: failed to declare `WF.foo` because `WF.foo.induct` has already been declared
+funind_reserved.lean:40:4-40:7: error: failed to declare `Mutual1.foo` because `Mutual1.foo.induct` has already been declared
+funind_reserved.lean:63:4-63:7: error: failed to declare `Mutual2.bar` because `Mutual2.bar.induct` has already been declared
+funind_reserved.lean:76:4-76:7: error: failed to declare `Mutual3.foo` because `Mutual3.foo.mutual_induct` has already been declared
+funind_reserved.lean:91:4-91:7: error: failed to declare `Nested.foo` because `Nested.foo.induct` has already been declared