E4207

Compiler diagnostic name: invalid_predicate.

无效的谓词表达式。

量词和其他仅用于证明的谓词形式属于 MoonBit 的验证语言。它们可以出现在 proof_assert、契约和 .mbtp 谓词定义等证明位置，但不能作为普通运行时表达式使用。

错误示例

下面的示例尝试将一个带量词的谓词绑定为普通值：

///|
fn invalid_predicate() -> Unit {
  let _ = ∀ i : Int, 0 <= i
}

///|
test {
  ignore(invalid_predicate)
}

MoonBit 会报告一个错误。

建议

将谓词移动到 proof_assert 等证明位置：

///|
fn checked_predicate() -> Unit {
  proof_assert ∀ i : Int, i == i
}

///|
test {
  checked_predicate()
}