# 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]`.fnfill['count':int32]->list[int32][min0,max5]orfail[too_many]{if'count'>5{failtoo_many;}letmut'out':=list.empty;for'i'from1to'count'by1{list.append[lend.mut'out',value'i'times'i'];}returngive'out';}MAIN{letmut'squares':list[int32][min0,max5]=fill[3]otherwiselist.empty;let'n':=list.length[lend'squares'];# a uint64[min 0, max 5]let'small':int8='n';# proven: the bound says at most 5std::print.useful['squares'," has ",'small',newln];list.append[lend.mut'squares',value16];list.append[lend.mut'squares',value25];# five: still insidestd::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];}