关于：`ctorResultingTypeMismatch`🔗

Error code: lean.ctorResultingTypeMismatch

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

Severity: ErrorSince: 4.22.0

在归纳声明中，每个构造函数的结果类型必须与正在的类型匹配宣布；如果不存在，则会引发此错误。也就是说，归纳类型的每个构造函数都必须返回该类型的值。请参阅归纳类型手册部分了解额外的细节。请注意，如果以下情况，可以省略构造函数的结果类型： inductive type being defined has no indices.

示例🔗

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.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 α

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)

如果构造函数的类型被注释，则完整类型（包括结果类型）必须是提供。或者，可以使用命名绑定器编写构造函数参数；这允许省略构造函数的结果类型，因为它不包含索引。

关于：ctorResultingTypeMismatch🔗

示例🔗

关于：`ctorResultingTypeMismatch`🔗