Macros§
Structs§
- Seq
Seq<A>
is a sequence type for specifications. To use a “sequence” in compiled code, use anexec
type likevec::Vec
that hasSeq<A>
as its specification type.
Functions§
- axiom_
seq_ add_ index1 - axiom_
seq_ add_ index2 - axiom_
seq_ add_ len - axiom_
seq_ empty - axiom_
seq_ ext_ equal - axiom_
seq_ ext_ equal_ deep - axiom_
seq_ index_ decreases - axiom_
seq_ len_ decreases - axiom_
seq_ new_ index - axiom_
seq_ new_ len - axiom_
seq_ push_ index_ different - axiom_
seq_ push_ index_ same - axiom_
seq_ push_ len - axiom_
seq_ subrange_ decreases - axiom_
seq_ subrange_ index - axiom_
seq_ subrange_ len - axiom_
seq_ update_ different - axiom_
seq_ update_ len - axiom_
seq_ update_ same - group_
seq_ axioms