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

all

True when ``p`` holds for every element of ``l``.
def all (p : (x : a) → Bool) (l : List a) : Bool