`lean.ctorResultingTypeMismatch`

Resulting type of constructor was not the inductive type being declared.

Severity: ErrorSince: 4.22.0

In an inductive declaration, the resulting type of each constructor must match the type being declared; if it does not, this error is raised. That is, every constructor of an inductive type must return a value of that type. See the Inductive Types manual section for additional details. Note that it is possible to omit the resulting type for a constructor if the inductive type being defined has no indices.

Examples

Typo in resulting type

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Unexpected resulting type for constructor 'Tree.node': Expected an application of
  Tree
but found
  ?m.22α → Tree α → Treee α

Unexpected resulting type for constructor 'Tree.node': Expected an application of
  Tree
but found
  ?m.22

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : α → Tree α → Tree α

Missing resulting type after constructor parameter

inductive Credential where
  | pin      : Unexpected resulting type for constructor 'Credential.pin': Expected
  Credential
but found
  NatNat
  | password : String

Unexpected resulting type for constructor 'Credential.pin': Expected
  Credential
but found
  Nat

inductive Credential where
  | pin      : Nat → Credential
  | password : String → Credential

inductive Credential where
  | pin (num : Nat)
  | password (str : String)

If the type of a constructor is annotated, the full type—including the resulting type—must be provided. Alternatively, constructor parameters can be written using named binders; this allows the omission of the constructor's resulting type because it contains no indices.