Seqs: Issues and Examples

Seq Specs

Basic Seqs: The seqs are constructed from containers; see containers for the full construction.
Two sorts: E (element) and Seq (container).
Core operations are:
op empty-seq : Seq
op singleton : E -> Seq
op concat : Seq, Seq -> Seq
Defined operations are:
op empty? : Seq -> Boolean
op nonempty? : Seq -> Boolean
op in : E, Seq -> Boolean
op prepend : E, Seq -> Seq

There are two constructor sets:
- empty, singleton, and concat
- empty, prepend
Seqs: Seqs import BASIC-SEQ. They add a new sort: NE-Seq. Also, they add the operations: head, tail, size, valid-index?, nth, exists, forall, reduce, image, filter
See containers
w-SEQ: w-SEQs (I.e., omega-seqs) on E are functions from Nat to E. There is an abstract sort, but the operations (eg, analogs of construct-seq, shadow-seq, apply-seq etc) are (usually) lambda operations on functions. See seq-of-rational.re and cauchy-seq.re for examples of use.