Testing: Tests from types

fn double(n: Int) -> Int
    require n >= 0 and n < 1_000_000
    ensure result >= n
    example double(21) == 42
{
    n * 2
}

✓ double: example double(21) == 421 passed, 0 failedseed 7✓ double  200 cases1 functions   1 ✓   0 ✗   0 weakly tested

Two hundred generated calls, each meeting the require and checked against the ensure, plus the example. The seed line lets anyone repeat the run exactly.

When no inputs are generated

Some functions get no generated arguments. The report lists each as not generated, with the reason:

• a generic function, or a method of a generic type;
• a parameter whose values can't be generated, such as a record holding a Shared, unless its type has a Sample;
• a capability with no fake yet;
• a C function, or a function a generated case found reaching C or raw memory (alloc, *p): they run only in native code.

When no generated input meets a function's require, its examples are what checks it, and the report says so:

/// The first item, or `none` for an empty list.
fn first<T>(items: [T]) -> T? {
    if items.is_empty() {
        return none
    }
    items[0]
}

/// How many seats are left.
fn left(seats: Shared<Int>) -> Int {
    seats.get()
}

/// The discount a code gives, in percent.
fn discount(code: String) -> Int
    require code.starts_with("SHOP-") and code.len() == 9
    example discount("SHOP-2026") == 10
{
    10
}

fn main() {
    print(first([3, 4]) ?? 0)
    print(left(Shared(2)))
    print(discount("SHOP-2026"))
}

✓ discount: example discount("SHOP-2026") == 101 passed, 0 failedseed 7✓ discount  checked by its examples only: no generated input met its `require`1 functions   1 ✓   0 ✗   0 weakly tested  not generated: first: generic  not generated: left: takes values that can't be generated yet