chore: deprecate variants other than inductive ... where

src/Init/Core.lean

@@ -1124,7 +1124,7 @@ The transitive closure `TransGen r` of a relation `r` is the smallest relation w
 transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
 `a r b r ... r z` of length at least 1 connecting `a` to `z`.
 -/
-inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
+inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop where
   /-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
   | single {a b} : r a b → TransGen r a b
   /-- The transitive closure is transitive. -/

src/Init/Data/AC.lean

@@ -9,7 +9,7 @@ import Init.Classical
 import Init.ByCases
 
 namespace Lean.Data.AC
-inductive Expr
+inductive Expr where
   | var (x : Nat)
   | op (lhs rhs : Expr)
   deriving Inhabited, Repr, BEq

src/Init/Data/List/Basic.lean

@@ -682,7 +682,7 @@ def notElem [BEq α] (a : α) (as : List α) : Bool :=
 Unlike `elem`, this uses `=` instead of `==` and is suited for mathematical reasoning.
 * `a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z`
 -/
-inductive Mem (a : α) : List α → Prop
+inductive Mem (a : α) : List α → Prop where
   /-- The head of a list is a member: `a ∈ a :: as`. -/
   | head (as : List α) : Mem a (a::as)
   /-- A member of the tail of a list is a member of the list: `a ∈ l → a ∈ b :: l`. -/
@@ -882,7 +882,7 @@ instance [DecidableEq α] : DecidableRel (Subset : List α → List α → Prop)
 /-! ### Sublist and isSublist -/
 
 /-- `l₁ <+ l₂`, or `Sublist l₁ l₂`, says that `l₁` is a (non-contiguous) subsequence of `l₂`. -/
-inductive Sublist {α} : List α → List α → Prop
+inductive Sublist {α} : List α → List α → Prop where
   /-- the base case: `[]` is a sublist of `[]` -/
   | slnil : Sublist [] []
   /-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/
@@ -1040,7 +1040,7 @@ Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
 For example if `R = (·≠·)` then it asserts `l` has no duplicates,
 and if `R = (·<·)` then it asserts that `l` is (strictly) sorted.
 -/
-inductive Pairwise : List α → Prop
+inductive Pairwise : List α → Prop where
   /-- All elements of the empty list are vacuously pairwise related. -/
   | nil : Pairwise []
   /-- `a :: l` is `Pairwise R` if `a` `R`-relates to every element of `l`,
@@ -1252,7 +1252,7 @@ theorem lookup_cons [BEq α] {k : α} :
 `Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
 of each other. This is defined by induction using pairwise swaps.
 -/
-inductive Perm : List α → List α → Prop
+inductive Perm : List α → List α → Prop where
   /-- `[] ~ []` -/
   | nil : Perm [] []
   /-- `l₁ ~ l₂ → x::l₁ ~ x::l₂` -/

src/Init/Data/Option/Basic.lean

@@ -166,7 +166,7 @@ def liftOrGet (f : α → α → α) : Option α → Option α → Option α
 
 /-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
 `none ~ none`. -/
-inductive Rel (r : α → β → Prop) : Option α → Option β → Prop
+inductive Rel (r : α → β → Prop) : Option α → Option β → Prop where
   /-- If `a ~ b`, then `some a ~ some b` -/
   | some {a b} : r a b → Rel r (some a) (some b)
   /-- `none ~ none` -/

src/Init/Prelude.lean

@@ -1646,7 +1646,7 @@ def Nat.ble : @& Nat → @& Nat → Bool
 An inductive definition of the less-equal relation on natural numbers,
 characterized as the least relation `≤` such that `n ≤ n` and `n ≤ m → n ≤ m + 1`.
 -/
-protected inductive Nat.le (n : Nat) : Nat → Prop
+protected inductive Nat.le (n : Nat) : Nat → Prop where
   /-- Less-equal is reflexive: `n ≤ n` -/
   | refl     : Nat.le n n
   /-- If `n ≤ m`, then `n ≤ m + 1`. -/

src/Init/System/IO.lean

@@ -211,7 +211,7 @@ def sleep (ms : UInt32) : BaseIO Unit :=
 @[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit
 
 /-- The current state of a `Task` in the Lean runtime's task manager. -/
-inductive TaskState
+inductive TaskState where
   /--
   The `Task` is waiting to be run.
   It can be waiting for dependencies to complete or

src/Lean/Attributes.lean

@@ -37,7 +37,7 @@ This is used to indicate how an attribute should be scoped.
 Note that the attribute handler (`AttributeImpl.add`) is responsible for interpreting the kind and
 making sure that these kinds are respected.
 -/
-inductive AttributeKind
+inductive AttributeKind where
   | global | local | scoped
   deriving BEq, Inhabited
 

src/Lean/Data/Json/Printer.lean

@@ -68,7 +68,7 @@ end
 def pretty (j : Json) (lineWidth := 80) : String :=
   Format.pretty (render j) lineWidth
 
-protected inductive CompressWorkItem
+protected inductive CompressWorkItem where
   | json (j : Json)
   | arrayElem (j : Json)
   | arrayEnd

src/Lean/Data/Lsp/CodeActions.lean

@@ -32,7 +32,7 @@ You can make your own code action kinds, the ones supported by LSP are:
 -/
 abbrev CodeActionKind := String
 
-inductive CodeActionTriggerKind
+inductive CodeActionTriggerKind where
   /-- Code actions were explicitly requested by the user or by an extension. -/
   | invoked
   /-- Code actions were requested automatically.

src/Lean/Data/Lsp/Extra.lean

@@ -52,7 +52,7 @@ instance : FromJson WaitForDiagnostics :=
 instance : ToJson WaitForDiagnostics :=
   ⟨fun _ => mkObj []⟩
 
-inductive LeanFileProgressKind
+inductive LeanFileProgressKind where
   | processing | fatalError
   deriving Inhabited, BEq
 

src/Lean/Data/Lsp/Internal.lean

@@ -34,7 +34,7 @@ inductive RefIdent where
 namespace RefIdent
 
 /-- Shortened representation of `RefIdent` for more compact serialization. -/
-inductive RefIdentJsonRepr
+inductive RefIdentJsonRepr where
   /-- Shortened representation of `RefIdent.const` for more compact serialization. -/
   | c (m n : String)
   /-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/

src/Lean/Data/Lsp/Workspace.lean

@@ -41,7 +41,7 @@ structure DidChangeWatchedFilesRegistrationOptions where
   watchers : Array FileSystemWatcher
   deriving FromJson, ToJson
 
-inductive FileChangeType
+inductive FileChangeType where
   | Created
   | Changed
   | Deleted

src/Lean/Data/NameTrie.lean

@@ -8,7 +8,7 @@ import Lean.Data.PrefixTree
 
 namespace Lean
 
-inductive NamePart
+inductive NamePart where
   | str (s : String)
   | num (n : Nat)
 

src/Lean/Data/Xml/Basic.lean

@@ -14,13 +14,13 @@ def Attributes := RBMap String String compare
 instance : ToString Attributes := ⟨λ as => as.fold (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩
 
 mutual
-inductive Element
+inductive Element where
 | Element
   (name : String)
   (attributes : Attributes)
   (content : Array Content)
 
-inductive Content
+inductive Content where
 | Element (element : Element)
 | Comment (comment : String)
 | Character (content : String)

src/Lean/Elab/Declaration.lean

@@ -11,6 +11,7 @@ import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.MutualDef
 import Lean.Elab.DeclarationRange
+import Lean.Linter.Deprecated
 namespace Lean.Elab.Command
 
 open Meta
@@ -136,7 +137,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
 /-
-leading_parser "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
+leading_parser "inductive " >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
 leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
@@ -167,6 +168,12 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
   let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  unless ctors.isEmpty || decl[3][0].isToken "where" do
+   -- https://github.com/leanprover/lean4/issues/5236 decided to deprecate all other variants
+    if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
+      withRef decl[0] <| withRef decl[3] <| logWarning <| .tagged ``Linter.deprecatedAttr "\
+        Variants other than 'inductive ... where' have been deprecated.\n\
+        You can disable this warning with 'set_option linter.deprecated false'."
   return {
     ref             := decl
     shortDeclName   := name

src/Lean/Elab/GuardMsgs.lean

@@ -40,7 +40,7 @@ private def messageToStringWithoutPos (msg : Message) : IO String := do
   return str
 
 /-- The decision made by a specification for a message. -/
-inductive SpecResult
+inductive SpecResult where
   /-- Capture the message and check it matches the docstring. -/
   | check
   /-- Drop the message and delete it. -/
@@ -49,7 +49,7 @@ inductive SpecResult
   | passthrough
 
 /-- The method to use when normalizing whitespace, after trimming. -/
-inductive WhitespaceMode
+inductive WhitespaceMode where
   /-- Exact equality. -/
   | exact
   /-- Equality after normalizing newlines into spaces. -/
@@ -58,7 +58,7 @@ inductive WhitespaceMode
   | lax
 
 /-- Method to use when combining multiple messages. -/
-inductive MessageOrdering
+inductive MessageOrdering where
   /-- Use the exact ordering of the produced messages. -/
   | exact
   /-- Sort the produced messages. -/

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -401,7 +401,7 @@ def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
 
 /-- A `GuessLexRel` described how a recursive call affects a measure; whether it
 decreases strictly, non-strictly, is equal, or else.  -/
-inductive GuessLexRel | lt | eq | le | no_idea
+inductive GuessLexRel where | lt | eq | le | no_idea
 deriving Repr, DecidableEq
 
 instance : ToString GuessLexRel where

src/Lean/Elab/Tactic/Guard.lean

@@ -18,7 +18,7 @@ The various `guard_*` tactics have similar matching specifiers for how equal exp
 have to be to pass the tactic.
 This inductive gives the different specifiers that can be selected.
 -/
-inductive MatchKind
+inductive MatchKind where
 /-- A syntactic match means that the `Expr`s are `==` after stripping `MData` -/
 | syntactic
 /-- A defeq match `isDefEqGuarded` returns true. (Note that unification is allowed here.) -/

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -36,7 +36,7 @@ abbrev Proof : Type := OmegaM Expr
 Our internal representation of an argument "justifying" that a constraint holds on some coefficients.
 We'll use this to construct the proof term once a contradiction is found.
 -/
-inductive Justification : Constraint → Coeffs → Type
+inductive Justification : Constraint → Coeffs → Type where
   /--
   `Problem.assumptions[i]` generates a proof that `s.sat' coeffs atoms`
   -/

src/Lean/Elab/Tactic/RCases.lean

@@ -53,7 +53,7 @@ the type being destructed, the extra patterns will match on the last element, me
 `p1 | p2 | p3` will act like `p1 | (p2 | p3)` when matching `a1 ∨ a2 ∨ a3`. If matching against a
 type with 3 constructors,  `p1 | (p2 | p3)` will act like `p1 | (p2 | p3) | _` instead.
 -/
-inductive RCasesPatt : Type
+inductive RCasesPatt : Type where
   /-- A parenthesized expression, used for hovers -/
   | paren (ref : Syntax) : RCasesPatt → RCasesPatt
   /-- A named pattern like `foo` -/

src/Lean/Elab/Term.lean

@@ -30,7 +30,7 @@ structure SavedContext where
   levelNames : List Name
 
 /-- The kind of a tactic metavariable, used for additional error reporting. -/
-inductive TacticMVarKind
+inductive TacticMVarKind where
   /-- Standard tactic metavariable, arising from `by ...` syntax. -/
   | term
   /-- Tactic metavariable arising from an autoparam for a function application. -/
@@ -1449,9 +1449,9 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   Reason: consider the following example
   ```
     mutual
-      inductive Foo
+      inductive Foo where
       | somefoo : Foo | bar : Bar → Foo → Foo
-      inductive Bar
+      inductive Bar where
       | somebar : Bar| foobar : Foo → Bar → Bar
     end
 

src/Lean/LocalContext.lean

@@ -15,7 +15,7 @@ namespace Lean
 Whether a local declaration should be found by type class search, tactics, etc.
 and shown in the goal display.
 -/
-inductive LocalDeclKind
+inductive LocalDeclKind where
   /--
   Participates fully in type class search, tactics, and is shown even if inaccessible.
 

src/Lean/Meta/CoeAttr.lean

@@ -24,7 +24,7 @@ is used, then `A.toB a` will be pretty-printed as `↑a`.
 namespace Lean.Meta
 
 /-- The different types of coercions that are supported by the `coe` attribute. -/
-inductive CoeFnType
+inductive CoeFnType where
   /-- The basic coercion `↑x`, see `CoeT.coe` -/
   | coe
   /-- The coercion to a function type, see `CoeFun.coe` -/

src/Lean/Meta/Tactic/AC/Main.lean

@@ -56,7 +56,7 @@ def preContext (expr : Expr) : MetaM (Option PreContext) := do
 
   return none
 
-inductive PreExpr
+inductive PreExpr where
 | op (lhs rhs : PreExpr)
 | var (e : Expr)
 

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -54,7 +54,7 @@ A "modifier" for a declaration.
   and we want to consider the forward direction,
 * `mpr` similarly, but for the backward direction.
 -/
-inductive DeclMod
+inductive DeclMod where
   | /-- the original declaration -/ none
   | /-- the forward direction of an `iff` -/ mp
   | /-- the backward direction of an `iff` -/ mpr

src/Lean/Meta/Tactic/NormCast.lean

@@ -15,7 +15,7 @@ namespace Lean.Meta.NormCast
 * move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
 * squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
 -/
-inductive Label
+inductive Label where
   /-- elim lemma: LHS has 0 head coes and ≥ 1 internal coe -/
   | elim
   /-- move lemma: LHS has 1 head coe and 0 internal coes,

src/Lean/Meta/Tactic/Rewrites.lean

@@ -156,7 +156,7 @@ private def RewriteResult.ppResult (r : RewriteResult) : MetaM String :=
 
 
 /-- Should we try discharging side conditions? If so, using `assumption`, or `solve_by_elim`? -/
-inductive SideConditions
+inductive SideConditions where
 | none
 | assumption
 | solveByElim

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -267,7 +267,7 @@ def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
   let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
   withBindingBody' n (mkAnnotatedIdent n) (d ·)
 
-inductive OmissionReason
+inductive OmissionReason where
   | deep
   | proof
   | maxSteps

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -334,7 +334,7 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
     return Syntax.mkApp fnStx argStxs
 
 /-- Records how a particular argument to a function is delaborated, in non-explicit mode. -/
-inductive AppImplicitArg
+inductive AppImplicitArg where
   /-- An argument to skip, like an implicit argument. -/
   | skip
   /-- A regular argument. -/

src/Lean/Server/CodeActions/Provider.lean

@@ -44,7 +44,7 @@ A code action which calls all `@[hole_code_action]` code actions on each hole
 The return value of `findTactic?`.
 This is the syntax for which code actions will be triggered.
 -/
-inductive FindTacticResult
+inductive FindTacticResult where
   /-- The nearest enclosing tactic is a tactic, with the given syntax stack. -/
   | tactic : Syntax.Stack → FindTacticResult
   /-- The cursor is between tactics, and the nearest enclosing range is a tactic sequence.

src/Lean/Server/GoTo.lean

@@ -13,7 +13,7 @@ namespace Lean.Server
 
 open Lsp
 
-inductive GoToKind
+inductive GoToKind where
   | declaration | definition | type
   deriving BEq, ToJson, FromJson
 

src/Lean/Server/Watchdog.lean

@@ -90,7 +90,7 @@ section Utils
     | crashed (e : IO.Error)
     | ioError (e : IO.Error)
 
-  inductive CrashOrigin
+  inductive CrashOrigin where
     | fileWorkerToClientForwarding
     | clientToFileWorkerForwarding
 

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -12,7 +12,7 @@ import Lean.Widget.InteractiveGoal
 namespace Lean.Widget
 open Lsp Server
 
-inductive StrictOrLazy (α β : Type) : Type
+inductive StrictOrLazy (α β : Type) : Type where
   | strict : α → StrictOrLazy α β
   | lazy : β → StrictOrLazy α β
   deriving Inhabited, RpcEncodable
@@ -93,7 +93,7 @@ that would effectively require reimplementing the (stateful, to keep track of in
 `Format.prettyM` algorithm.
 -/
 
-private inductive EmbedFmt
+private inductive EmbedFmt where
   /-- Nested tags denote `Info` objects in `infos`. -/
   | code (ctx : Elab.ContextInfo) (infos : RBMap Nat Elab.Info compare)
   /-- Nested text is ignored. -/