# E0039

Warning name: `missing_reasoning`

This warning is emitted for a proof-checked `for` loop that has no
`proof_reasoning` clause. Proof reasoning records the argument that explains why
the loop invariants are maintained and why the loop result satisfies the
surrounding contract.

## Erroneous example

The loop does not have a `proof_reasoning` clause.

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

## Suggestion

Add some proof reasoning.

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