`lean.inductiveParamMissing`

Parameter not present in an occurrence of an inductive type in one of its constructors.

Severity: ErrorSince: 4.22.0

This error occurs when an inductive type constructor is partially applied in the type of one of its constructors such that one or more parameters of the type are omitted. The elaborator requires that all parameters of an inductive type be specified everywhere that type is referenced in its definition, including in the types of its constructors.

If it is necessary to allow the type constructor to be partially applied, without specifying a given type parameter, that parameter must be converted to an index. See the manual section on Inductive Types for further explanation of the difference between indices and parameters.

Examples

Omitting parameter in argument to higher-order predicate

inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
  | nil : All P []
  | cons {x xs} : P x → All P xs → All P (x :: xs)

structure RoseTree (α : Type u) where
  val : α
  children : List (RoseTree α)

inductive RoseTree.All {α : Type u} (P : α → Prop) (t : RoseTree α) : Prop
  | intro : P t.val → List.All (All P) t.children → All P t

<invalid output>

inductive List.All {α : Type u} (P : α → Prop) : List α → Prop
  | nil : All P []
  | cons {x xs} : P x → All P xs → All P (x :: xs)

structure RoseTree (α : Type u) where
  val : α
  children : List (RoseTree α)

inductive RoseTree.All {α : Type u} (P : α → Prop) : RoseTree α → Prop
  | intro : P t.val → List.All (All P) t.children → All P t

Because the RoseTree.All type constructor must be partially applied in the argument to List.All, the unspecified argument (t) must not be a parameter of the RoseTree.All predicate. Making it an index to the right of the colon in the header of RoseTree.All allows this partial application to succeed.