Seq

A persistent sequence with unrestricted element types and no abstract refinement parameters. Useful for higher-order programs and nested ADTs.
Table of Contents

Types

Seq

(inductive)
A persistent sequence with unrestricted element types and no abstract refinement parameters. Useful for higher-order programs and nested ADTs.
inductive Seq a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Seq (inductive)

nil

constructor
(Seq a)

cons

constructor
(Seq a)

Functions

length

def length (xs : (Seq a)) : Int

empty

def empty (xs : (Seq a)) : Bool

append

def append (xs : (Seq a)) (ys : (Seq a)) : (Seq a)

map

def map (f : (x : a) → b) (xs : (Seq a)) : (Seq b)

foldr

def foldr (f : (x : a) → (acc : b) → b) (z : b) (xs : (Seq a)) : b

reverseAcc

def reverseAcc (xs : (Seq a)) (acc : (Seq a)) : (Seq a)

reverse

def reverse (xs : (Seq a)) : (Seq a)

snoc

def snoc (xs : (Seq a)) (x : a) : (Seq a)