← All examples

A length bound on a list

list[T][lo, hi].

bounded.zg
# A length bound on a list: `list[T][lo, hi]` (decided 2026-09-21).
# Like `int32[min 0, max 100]`: the thing, then its bounds. Its length is a `uint64[lo, hi]`.

fn fill ['count': int32] -> list[int32][min 0, max 5] or fail[too_many] {
    if 'count' > 5 { fail too_many; }
    let mut 'out' := list.empty;
    for 'i' from 1 to 'count' by 1 { list.append[lend.mut 'out', value 'i' times 'i']; }
    return give 'out';
}

MAIN {
    let mut 'squares': list[int32][min 0, max 5] = fill[3] otherwise list.empty;
    let 'n' := list.length[lend 'squares'];    # a uint64[min 0, max 5]
    let 'small': int8 = 'n';                   # proven: the bound says at most 5
    std::print.useful['squares', " has ", 'small', newln];
    list.append[lend.mut 'squares', value 16];
    list.append[lend.mut 'squares', value 25];       # five: still inside
    std::print.useful[list.length[lend 'squares'], newln];
    let 'big' := fill[9] otherwise { too_many { std::print.useful["9 is too many", newln]; std::exit[0]; } };
    std::print.useful[list.length[lend 'big'], newln];
}
Output
[1, 4, 9] has 3
5
9 is too many