关于：`ctorResultingTypeMismatch`🔗

Error code: lean.ctorResultingTypeMismatch

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

Severity: ErrorSince: 4.22.0

在归纳声明中，每个构造器的结果类型必须与所声明的类型匹配；否则就会产生此错误。也就是说，归纳类型的每个构造器都必须返回该类型的值。更多信息请参阅归纳类型。注意，如果所定义的归纳类型没有索引，可以省略构造器的结果类型。

示例🔗

结果类型中的拼写错误

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

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

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

构造器参数后缺少结果类型

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)

如果标注了构造器类型，就必须提供完整类型（包括结果类型）。另一种方式是使用命名绑定项书写构造器参数；这样便可省略不含索引的构造器结果类型。

关于：ctorResultingTypeMismatch🔗

示例🔗

关于：`ctorResultingTypeMismatch`🔗