E4196

编译器诊断名称：where_clause_reasoning_not_string。

where 子句中的 proof_reasoning 字段用于记录证明的说明文本。它的值必须是字符串字面量或多行字符串字面量，不能是变量或其他表达式。

错误示例

///|
fn keep(
  x : Int,
) -> Int where {
  proof_ensure: result => result == x,
  proof_reasoning: x,
} {
  x
}

///|
test {
  ignore(keep)
}

建议

为 proof_reasoning 使用字符串字面量。

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

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