# 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](/language/verification.md), especially
[Contracts in `.mbt`](/language/verification.md#contracts-in-mbt) and
[Loop Invariants](/language/verification.md#loop-invariants).

## Erroneous example

```{literalinclude} /sources/error_codes/4195_error/top.mbt
:language: moonbit
```

## Suggestion

Replace the unknown field with a supported `where` clause field.

```{literalinclude} /sources/error_codes/4195_fixed/top.mbt
:language: moonbit
```