# 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:

```{literalinclude} /sources/error_codes/4207_error/top.mbt
:language: text
```

MoonBit will report an error.

## Suggestion

Move the predicate into a proof position such as `proof_assert`:

```{literalinclude} /sources/error_codes/4207_fixed/top.mbt
:language: text
```