List

Linked list — an inductive datatype with the standard ``nil`` / ``cons`` constructors and a length measure. ``List`` is parameterised by: * its element type ``a``; * an abstract refinement ``p`` (Liquid Haskell-style ``data List a <p>``) that every element of the list satisfies. The refinement flows through every constructor: a value can only enter the list if it satisfies ``p``.
Table of Contents

Types

List

(inductive)
Linked list — an inductive datatype with the standard ``nil`` / ``cons`` constructors and a length measure. ``List`` is parameterised by: * its element type ``a``; * an abstract refinement ``p`` (Liquid Haskell-style ``data List a <p>``) that every element of the list satisfies. The refinement flows through every constructor: a value can only enter the list if it satisfies ``p``.
inductive List a forall <p:(_ : a) -> Bool -> Bool>
Measures
size : Int

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.

List (inductive)

nil

constructor
{l : List a | size l == 0}

cons

constructor
{l : List a | size l == size tl + 1}

Functions

length

Length of the list (counted by recursion).
def length (l: List a) : Int

empty

True when the list is empty.
def empty (l: List a) : Bool

append

Append two lists.
def append (xs: List a) (ys: List a) : List a

map

Map a function over the list.
def map (f: (x : a) -> b) (l: List a) : List b

foldr

Right fold: ``foldr f z [x1, ..., xn] == f x1 (f x2 (... (f xn z)))``.
def foldr (f: (x : a) -> (acc : b) -> b) (z: b) (l: List a) : b

reverse_acc

Reverse helper: prepends elements of ``xs`` onto ``acc``.
def reverse_acc (xs: List a) (acc: List a) : List a

reversed

Reverse a list.
def reversed (l: List a) : List a

snoc

Append a value at the back of the list (snoc).
def snoc (l: List a) (x: a) : List a

sum

Sum of a list of integers.
def sum (l: List Int) : Int