Lean 语言参考

关于：inferDefTypeFailed🔗

Error code: lean.inferDefTypeFailed

The type of a definition could not be inferred.

Severity: ErrorSince: 4.23.0

当未完全指定定义的类型且 Lean 无法推断时，会出现此错误 从可用信息中可以看出其类型。如果定义有参数，这个错误仅指 冒号后的结果类型（错误 lean.inferBinderTypeFailed 表示无法推断参数类型）。

要解决此错误，请在定义中提供附加类型信息。这可以做到 直接通过在定义中的冒号后提供显式结果类型来实现 标头。或者，如果未提供显式结果类型，则添加更多类型 定义主体的信息——例如通过指定隐式类型参数或给出 let 绑定器的显式类型 — 可以允许 Lean 推断定义的类型。寻找类型 与此一起出现的推理或隐式论证综合错误，以识别 可能导致此错误的歧义。

请注意，当提供显式结果类型时（即使该类型包含孔），Lean 也不会 使用定义主体中的信息来帮助推断定义或其参数的类型。 因此，添加显式结果类型可能还需要向参数添加类型注释 其类型以前是可以推断的。此外，始终需要提供明确的 输入 theorem 声明：theorem 语法需要类型注释，而精化器 永远不会尝试使用定理体来推断被证明的命题。

示例🔗

Implicit Argument Cannot be Inferred
def Failed to infer type of definition `emptyNats`emptyNats := don't know how to synthesize implicit argument `α` @List.nil ?m.3 context: ⊢ Type u_1[] 
Failed to infer type of definition `emptyNats`
def emptyNats : List Nat := []
def emptyNats := List.nil (α := Nat)

这里，Lean 无法推断出 List 类型构造函数的参数 α 的值，即 反过来又阻止它推断定义的类型。可能有两种修复方法：指定 定义的预期类型允许 Lean 推断适当的隐式参数 List.nil 构造函数；或者，使这个隐式参数在函数体中显式显示 为 Lean 提供足够的信息来推断定义的类型。

Definition Type Uninferrable Due to Unknown Parameter Type
def Failed to infer type of definition `identity`identity Failed to infer type of binder `x`x := x 
Failed to infer type of definition `identity`
def identity (x : α) := x

在此示例中，identity 的类型由 x 的类型确定，无法推断。 指示的错误和 lean.inferBinderTypeFailed 因此出现（请参阅该示例的其他讨论的解释）。解决 后者通过显式指定 x 的类型为 Lean 提供足够的信息来推断 定义类型。