E4207

Compiler diagnostic name: invalid_predicate.

Invalid predicate expression.

Quantifiers and other proof-only predicate forms are part of MoonBit's verification language. They are valid in proof positions such as proof_assert, contracts, and .mbtp predicate definitions, but they cannot be used as ordinary runtime expressions.

Erroneous example

The following example tries to bind a quantified predicate as an ordinary value:

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

///|
test {
  ignore(invalid_predicate)
}

MoonBit will report an error.

Suggestion

Move the predicate into a proof position such as proof_assert:

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

///|
test {
  checked_predicate()
}