E4195

编译器诊断名称：invalid_where_clause_field。

where 子句只接受当前上下文中有意义的字段。对于函数契约，请使用 proof_require、proof_ensure、proof_decrease、proof_axiomatized 和 proof_reasoning 等字段。对于循环契约，请使用 proof_invariant、proof_yield 和 proof_reasoning 等字段。

关于这些字段背后的证明概念，请参阅形式化验证，尤其是 .mbt 中的契约 和循环不变式。

错误示例

///|
fn keep(x : Int) -> Int where { proof_note: x >= 0 } {
  x
}

///|
test {
  ignore(keep)
}

建议

将未知字段替换为支持的 where 子句字段。

///|
fn keep(
  x : Int,
) -> Int where {
  proof_require: x >= 0,
  proof_ensure: result => result == x,
  proof_reasoning: "The function returns its argument unchanged.",
} {
  x
}

///|
test {
  inspect(keep(1), content="1")
}