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``.
Imports
open Copy;
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
structuralRank : Int
first : a
rest : (List 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.

List (inductive)

nil

constructor
{l : (List a) | size l = 0 && structuralRank l = 0}

cons

constructor
{ l : (List a) | size l = size tl + 1 && structuralRank l = structuralRank tl + 1 && structuralRank tl ≥ 0 && first l = hd && rest l = tl }

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