E4195

Compiler diagnostic name: invalid_where_clause_field.

A where clause accepts only the fields that are meaningful for that context. For a function contract, use fields such as proof_require, proof_ensure, proof_decrease, proof_axiomatized, and proof_reasoning. For a loop contract, use fields such as proof_invariant, proof_yield, and proof_reasoning.

For the proof concepts behind these fields, see Formal Verification, especially Contracts in .mbt and Loop Invariants.

Erroneous example

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

///|
test {
  ignore(keep)
}

Suggestion

Replace the unknown field with a supported where clause field.

///|
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")
}