E4196

Compiler diagnostic name: where_clause_reasoning_not_string.

The proof_reasoning field in a where clause records explanatory text for the proof. Its value must be a string literal or a multiline string literal, not a variable or another expression.

Erroneous example

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

///|
test {
  ignore(keep)
}

Suggestion

Use a string literal for 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")
}