E0110

An ensures clause without a |r| binding for the return value.

Machine-applicable fix: none.

Example

This program fails with E0110.

fn double(n: Int) -> Int
    ensures r > 0
{
    n * 2
}

Fixed

The same program, fixed.

fn double(n: Int) -> Int
    ensures |r| r > 0
{
    n * 2
}

Listed in the checker notes. oskac explain E0110 prints this entry offline.

All error codes