E0281

A requires or ensures condition whose type is not Bool. Spans the condition.

Machine-applicable fix: none.

Example

This program fails with E0281.

fn run(n: Int) -> Int
    requires n
{
    n
}

Fixed

The same program, fixed.

fn run(n: Int) -> Int
    requires n > 0
{
    n
}

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

All error codes