Lean 语言参考手册

关于：dependsOnNoncomputable🔗

Error code: lean.dependsOnNoncomputable

Declaration depends on noncomputable definitions but is not marked as noncomputable

Severity: ErrorSince: 4.22.0

此错误表示指定的定义依赖一个或多个不包含可执行代码的定义，因此必须标记为 noncomputable。这类定义可以通过类型检查，但不包含可由 Lean 执行的代码。

如果你本来就打算让错误消息中命名的定义不可计算，将其标记为 noncomputable 即可解决此错误。 否则，请检查它所依赖的不可计算定义：它们可能因编译失败、是 axiom，或自身被标记为 noncomputable 而不可计算。让定义的所有不可计算依赖变为可计算也能解决此错误。 关于不可计算定义的更多信息，请参阅 修饰符章节。

示例🔗

必然不可计算的函数未正确标记
axiom transform : Nat → Nat def `transform` not supported by code generator; consider marking definition as `noncomputable`transformIfZero : Nat → Nat | 0 => transform 0 | n => n 
`transform` not supported by code generator; consider marking definition as `noncomputable`
axiom transform : Nat → Nat noncomputable def transformIfZero : Nat → Nat | 0 => transform 0 | n => n

在此例中，transformIfZero 依赖公理 transform。由于 transform 是公理，它不包含可执行代码； 虽然值 transform 0 的类型是 Nat，却无法计算其值。因此，transformIfZero 必须标记为 noncomputable， 因为执行它将依赖此公理。

不可计算依赖可以变为可计算
noncomputable def getOrDefault [Nonempty α] : Option α → α | some x => x | none => Classical.ofNonempty def failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'endsOrDefault (ns : List Nat) : Nat × Nat := let head := getOrDefault ns.head? let tail := getOrDefault ns.getLast? (head, tail) 
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'
def getOrDefault [Inhabited α] : Option α → α | some x => x | none => default def endsOrDefault (ns : List Nat) : Nat × Nat := let head := getOrDefault ns.head? let tail := getOrDefault ns.getLast? (head, tail)

getOrDefault 的原始定义因使用 Classical.choice 而不可计算。 不过，与前一个例子不同，可以实现一个类似但可计算的 getOrDefault 版本（使用 Inhabited 类型类）， 从而使 endsOrDefault 可计算。（Inhabited 与 Nonempty 的差异见 基本类章节中关于可居住类型的文档。）

命名空间中的不可计算实例
open Classical in /-- 如果 `y` 在 `f` 的像中，则返回 `y`； 否则返回 `f` 的像中的一个元素。 -/ def failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'fromImage (f : Nat → Nat) (y : Nat) := if ∃ x, f x = y then y else f 0 
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
open Classical in /-- 如果 `y` 在 `f` 的像中，则返回 `y`； 否则返回 `f` 的像中的一个元素。 -/ noncomputable def fromImage (f : Nat → Nat) (y : Nat) := if ∃ x, f x = y then y else f 0

Classical 命名空间包含不可计算的 Decidable 实例。这些实例常导致定义依赖源代码中未显式出现的 不可计算项。例如在上例中，命题的 Decidable 实例 ∃ x, f x = y 使用 Classical 判定实例进行实例合成；因此，fromImage 必须标记为 noncomputable。