Add Seq<T> as a model of Vec<T>#143

Merged

coord-e merged 5 commits into

mainfrom

claude/nifty-newton-wfxz2e

Jun 23, 2026

Commits on Jun 23, 2026

Add Seq<T> ghost type

claude
authored and
coord-e
committed
Add basic Seq<T> operations: empty, singleton, len, push, indexing

claude
authored and
coord-e
committed
Add Seq<T>::concat via define-fun-rec

claude
authored and
coord-e
committed
Add some peephole optimization of tuple/array operations

coord-e
and
claude
committed
Use Seq<T> as the model of Vec<T>

claude
authored and
coord-e
committed