Currently only find, enumerate, any, count, iter_mut exist.
- map — transforms elements; fundamental for reasoning about element-wise operations
- filter — subset selection; pairs well with separation logic predicates
- fold / reduce — accumulation; essential for sum/product/aggregate proofs
- zip — parallel iteration (partially exists as list_zip in tuples)
- take / skip — bounded iteration; useful for loop bound reasoning
- all — universal quantification over collections (complement to any)
- chain — sequence concatenation
These are critical because loop-based verification is a core use case (see the MLKEM NTT proof skeleton).
Follow-up: prove the fusion laws : map(f).map(g) = map(g∘f), filter(p).filter(q) = filter(p∧q) which are exactly the kind of equational reasoning that makes a formal stdlib useful for program optimization proofs.
Currently only find, enumerate, any, count, iter_mut exist.
These are critical because loop-based verification is a core use case (see the MLKEM NTT proof skeleton).
Follow-up: prove the fusion laws :
map(f).map(g) = map(g∘f), filter(p).filter(q) = filter(p∧q)which are exactly the kind of equational reasoning that makes a formal stdlib useful for program optimization proofs.