Add documentation and examples to Prelude/

Prelude/Bool/and

@@ -1,3 +1,15 @@
+{-
+The `Bool/and` function returns `False` if there are any `False` elements in the
+`List` and returns `True` otherwise
+
+Examples:
+
+```
+./and ([True, False, True] : List Bool) = True
+
+./and ([] : List Bool) = False
+```
+-}
 let and : List Bool → Bool
     =   λ(xs : List Bool)
     →   List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True

Prelude/Bool/build

@@ -1,3 +1,14 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) = True
+
+./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False
+```
+-}
 let build : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
     =   λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)
     →   f Bool True False

Prelude/Bool/fold

@@ -1,3 +1,14 @@
+{-
+`fold` is essentially the same as `if`/`then`/else` except as a function
+
+Examples:
+
+```
+./fold True Integer 0 1 = 0
+
+./fold False Integer 0 1 = 1
+```
+-}
 let fold : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
     =   λ(b : Bool)
     →   λ(bool : Type)

Prelude/Bool/not

@@ -1,3 +1,14 @@
+{-
+Flip the value of a `Bool`
+
+Examples:
+
+```
+./not True = False
+
+./not False = True
+```
+-}
 let not : Bool → Bool
     =   λ(b : Bool) → b == False
 

Prelude/Bool/or

@@ -1,3 +1,15 @@
+{-
+The `Bool/or` function returns `True` if there are any `True` elements in the
+`List` and returns `False` otherwise
+
+Examples:
+
+```
+./or ([True, False, True] : List Bool) = True
+
+./or ([] : List Bool) = False
+```
+-}
 let or : List Bool → Bool
     =   λ(xs : List Bool)
     →   List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False

Prelude/List/all

@@ -1,3 +1,15 @@
+{-
+Returns `True` if the supplied function returns `True` for all elements in the
+`List`
+
+Examples:
+
+```
+./all Natural Natural/even ([+2, +3, +5] : List Natural) = False
+
+./all Natural Natural/even ([] : List Natural) = True
+```
+-}
 let all : ∀(a : Type) → (a → Bool) → List a → Bool
     =   λ(a : Type)
     →   λ(f : a → Bool)

Prelude/List/any

@@ -1,3 +1,15 @@
+{-
+Returns `True` if the supplied function returns `True` for any element in the
+`List`
+
+Examples:
+
+```
+./any Natural Natural/even ([+2, +3, +5] : List Natural) = True
+
+./any Natural Natural/even ([] : List Natural) = False
+```
+-}
 let any : ∀(a : Type) → (a → Bool) → List a → Bool
     =   λ(a : Type)
     →   λ(f : a → Bool)

Prelude/List/build

@@ -1,3 +1,28 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+Text
+(   λ(list : Type)
+→   λ(cons : Text → list → list)
+→   λ(nil : list)
+→   cons "ABC" (cons "DEF" nil)
+)
+= ["ABC", "DEF"] : List Text
+
+./build
+Text
+(   λ(list : Type)
+→   λ(cons : Text → list → list)
+→   λ(nil : list)
+→   nil
+)
+= [] : List Text
+```
+-}
 let build
     :   ∀(a : Type)
     →   (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)

Prelude/List/concat

@@ -1,3 +1,28 @@
+{-
+Concatenate a `List` of `List`s into a single `List`
+
+Examples:
+
+```
+./concat Integer
+(   [   [0, 1, 2]    : List Integer
+    ,   [3, 4]       : List Integer
+    ,   [5, 6, 7, 8] : List Integer
+    ]   : List (List Integer)
+)
+= [0, 1, 2, 3, 4, 5, 6, 7, 8] : List Integer
+
+./concat Integer
+(   [   [] : List Integer
+    ,   [] : List Integer
+    ,   [] : List Integer
+    ]   : List (List Integer)
+)
+= [] : List Integer
+
+./concat Integer ([] : List (List Integer)) = [] : List Integer
+```
+-}
 let concat : ∀(a : Type) → List (List a) → List a
     =   λ(a : Type)
     →   λ(xss : List (List a))

Prelude/List/concatMap

@@ -1,3 +1,20 @@
+{-
+This is a convenience function that combines `concat` and `map`
+
+```
+./concatMap a b f xs = ./concat b (./map a b f xs)
+```
+
+Examples:
+
+```
+./concatMap Integer Integer (./replicate +3 Integer) ([0, 1, 2] : List Integer)
+= [0, 0, 0, 1, 1, 1, 2, 2, 2] : List Integer
+
+./concatMap Bool Bool (λ(x : Bool) → [] : List Bool) ([True, False] : List Bool)
+= [] : List Bool
+```
+-}
 let concatMap : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b
     =   λ(a : Type)
     →   λ(b : Type)

Prelude/List/filter

@@ -1,3 +1,16 @@
+{-
+Only keep elements of the list where the supplied function returns `True`
+
+Examples:
+
+```
+./filter Natural Natural/even ([+2, +3, +5] : List Natural)
+= [+2] : List Natural
+
+./filter Natural Natural/odd ([+2, +3, +5] : List Natural)
+= [+3, +5] : List Natural
+```
+-}
 let filter : ∀(a : Type) → (a → Bool) → List a → List a
     =   λ(a : Type)
     →   λ(f : a → Bool)

Prelude/List/fold

@@ -1,3 +1,39 @@
+{-
+`fold` is the primitive function for consuming `List`s
+
+If you treat the list `[x, y, z] : List t` as `cons x (cons y (cons z nil))`,
+then a `fold` just replaces each `cons` and `nil` with something else
+
+Examples:
+
+```
+    List/fold
+    Natural
+    ([+2, +3, +5] : List Natural)
+    Natural
+    (λ(x : Natural) → λ(y : Natural) → x + y)
+    +0
+=   +10
+
+    λ(nil : Natural)
+→   List/fold
+    Natural
+    ([+2, +3, +5] : List Natural)
+    Natural
+    (λ(x : Natural) → λ(y : Natural) → x + y)
+    nil
+=   λ(nil : Natural) → +2 + +3 + +5 + nil
+
+    λ(list : Type)
+→   λ(cons : Natural → list → list)
+→   λ(nil : list)
+→   List/fold Natural ([+2, +3, +5] : List Natural) list cons nil
+=   λ(list : Type)
+→   λ(cons : Natural → list → list)
+→   λ(nil : list)
+→   cons +2 (cons +3 (cons +5 nil))
+```
+-}
 let fold
     :   ∀(a : Type)
     →   List a

Prelude/List/generate

@@ -1,3 +1,15 @@
+{-
+Build a list by calling the supplied function on all `Natural` numbers from `+0`
+up to but not including the supplied `Natural` number
+
+Examples:
+
+```
+./generate +5 Bool Natural/even = [True, False, True, False, True] : List Bool
+
+./generate +0 Bool Natural/even = [] : List Bool
+```
+-}
 let generate : Natural → ∀(a : Type) → (Natural → a) → List a
     =   λ(n : Natural)
     →   λ(a : Type)

Prelude/List/head

@@ -1,3 +1,14 @@
+{-
+Retrieve the first element of the list
+
+Examples:
+
+```
+./head Integer ([0, 1, 2] : List Integer) = [0] : Optional Integer
+
+./head Integer ([] : List Integer) = [] : Optional Integer
+```
+-}
 let head : ∀(a : Type) → List a → Optional a
     =   List/head
 

Prelude/List/indexed

@@ -1,3 +1,19 @@
+{-
+Tag each element of the list with its index
+
+Examples:
+
+```
+./indexed Bool ([True, False, True] : List Bool)
+=   [   { index = +0, value = True  }
+    ,   { index = +1, value = False }
+    ,   { index = +2, value = True  }
+    ]   : List { index : Natural, value : Bool }
+
+./indexed Bool ([] : List Bool)
+= [] : List { index : Natural, value : Bool }
+```
+-}
 let indexed : ∀(a : Type) → List a → List { index : Natural, value : a }
     =   List/indexed
 

Prelude/List/iterate

@@ -1,3 +1,17 @@
+{-
+Generate a list of the specified length given a seed value and transition
+function
+
+Examples:
+
+```
+./iterate +10 Natural (λ(x : Natural) → x * +2) +1
+= [+1, +2, +4, +8, +16, +32, +64, +128, +256, +512] : List Natural
+
+./iterate +0 Natural (λ(x : Natural) → x * +2) +1
+= [] : List Natural
+```
+-}
 let iterate : Natural → ∀(a : Type) → (a → a) → a → List a
     =   λ(n : Natural)
     →   λ(a : Type)

Prelude/List/last

@@ -1,3 +1,14 @@
+{-
+Retrieve the last element of the list
+
+Examples:
+
+```
+./last Integer ([0, 1, 2] : List Integer) = [2] : Optional Integer
+
+./last Integer ([] : List Integer) = [] : Optional Integer
+```
+-}
 let last : ∀(a : Type) → List a → Optional a
     =   List/last
 

Prelude/List/length

@@ -1,3 +1,14 @@
+{-
+Returns the number of elements in a list
+
+Examples:
+
+```
+./length Integer ([0, 1, 2] : List Integer) = +3
+
+./length Integer ([] : List Integer) = +0
+```
+-}
 let length : ∀(a : Type) → List a → Natural
     =   List/length
 

Prelude/List/map

@@ -1,3 +1,15 @@
+{-
+Tranform a list by applying a function to each element
+
+Examples:
+
+```
+./map Natural Bool Natural/even ([+2, +3, +5] : List Natural)
+= [True, False, False] : List Bool
+
+./map Natural Bool Natural/even ([] : List Natural)
+```
+-}
 let map : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
     =   λ(a : Type)
     →   λ(b : Type)

Prelude/List/null

@@ -1,3 +1,14 @@
+{-
+Returns `True` if the `List` is empty and `False` otherwise
+
+Examples:
+
+```
+./null Integer ([0, 1, 2] : List Integer) = False
+
+./null Integer ([] : List Integer) = True
+```
+-}
 let null : ∀(a : Type) → List a → Bool
     =   λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)
 

Prelude/List/replicate

@@ -1,3 +1,14 @@
+{-
+Build a list by copying the given element the specified number of times
+
+Examples:
+
+```
+./replicate +9 Integer 1 = [1, 1, 1, 1, 1, 1, 1, 1, 1] : List Integer
+
+./replicate +0 Integer 1 = [] : List Integer
+```
+-}
 let replicate : Natural → ∀(a : Type) → a → List a
     =   λ(n : Natural)
     →   λ(a : Type)

Prelude/List/reversed

@@ -1,3 +1,14 @@
+{-
+Reverse a list
+
+Examples:
+
+```
+./reversed Integer ([0, 1, 2] : List Integer) = [2, 1, 0] : List Integer
+
+./reversed Integer ([] : List Integer) = [] : List Integer
+```
+-}
 let reversed : ∀(a : Type) → List a → List a
     =   List/reversed
 

Prelude/List/shifted

@@ -1,3 +1,41 @@
+{-
+Combine a `List` of `List`s, offsetting the `index` of each element by the
+number of elements in preceding lists
+
+Examples:
+
+```
+./shifted
+Bool
+(   [   [   { index = +0, value = True  }
+        ,   { index = +1, value = True  }
+        ,   { index = +2, value = True  }
+        ]   : List { index : Natural, value : Bool }
+    ,   [   { index = +0, value = False }
+        ,   { index = +1, value = False }
+        ]   : List { index : Natural, value : Bool }
+    ,   [   { index = +0, value = True  }
+        ,   { index = +1, value = True  }
+        ,   { index = +2, value = True  }
+        ,   { index = +3, value = True  }
+        ]   : List { index : Natural, value : Bool }
+    ]   : List (List { index : Natural, value : Bool })
+)
+=   [   { index = +0, value = True  }
+    ,   { index = +1, value = True  }
+    ,   { index = +2, value = True  }
+    ,   { index = +3, value = False }
+    ,   { index = +4, value = False }
+    ,   { index = +5, value = True  }
+    ,   { index = +6, value = True  }
+    ,   { index = +7, value = True  }
+    ,   { index = +8, value = True  }
+    ]   : List { index : Natural, value : Bool }
+
+./shifted Bool ([] : List (List { index : Natural, value : Bool }))
+= [] : List { index : Natural, value : Bool }
+```
+-}
 let shifted
     :   ∀(a : Type)
     →   List (List { index : Natural, value : a})

Prelude/List/unzip

@@ -1,3 +1,25 @@
+{-
+Unzip a list into two separate lists
+
+Examples:
+
+```
+./unzip
+Text
+Bool
+(   [   { _1 = "ABC", _2 = True  }
+    ,   { _1 = "DEF", _2 = False }
+    ,   { _1 = "GHI", _2 = True  }
+    ]   : List { _1 : Text, _2 : Bool }
+)
+=   { _1 = ["ABC", "DEF", "GHI"] : List Text
+    , _2 = [True, False, True] : List Bool
+    }
+
+./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
+= { _1 = [] : List Text, _2 = [] : List Bool }
+```
+-}
 let unzip
     :   ∀(a : Type)
     →   ∀(b : Type)

Prelude/Monoid

@@ -1,3 +1,37 @@
+{-
+Any function `f` that is a `Monoid` must satisfy the following law:
+
+```
+t  : Type
+f  : ./Monoid t
+xs : List (List t)
+
+f (./List/concat t xs) = f (./map (List t) t f xs)
+```
+
+Examples:
+
+```
+./Bool/and
+    : ./Monoid Bool
+./Bool/or
+    : ./Monoid Bool
+./List/concat
+    : ∀(a : Type) → ./Monoid (List a)
+./List/shifted
+    : ∀(a : Type) → ./Monoid (List { index : Natural, value : a })
+./Natural/sum
+    : ./Monoid Natural
+./Natural/product
+    : ./Monoid Natural
+./Optional/head
+    : ∀(a : Type) → ./Monoid (List (Optional a))
+./Optional/last
+    : ∀(a : Type) → ./Monoid (List (Optional a))
+./Text/concat
+    : ./Monoid Text
+```
+-}
 let Monoid : ∀(m : Type) → Type
     =   λ(m : Type) → List m → m
 

Prelude/Natural/build

@@ -1,3 +1,26 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+(   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   succ (succ (succ zero))
+)
+= +3
+
+./build
+(   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   zero
+)
+= +0
+```
+-}
 let build
     :   (   ∀(natural : Type)
         →   ∀(succ : natural → natural)

Prelude/Natural/enumerate

@@ -1,3 +1,15 @@
+{-
+Generate a list of numbers from `+0` up to but not including the specified
+number
+
+Examples:
+
+```
+./enumerate +10 = [+0, +1, +2, +3, +4, +5, +6, +7, +8, +9] : List Natural
+
+./enumerate +0 = [] : List Natural
+```
+-}
 let enumerate : Natural → List Natural
     =   λ(n : Natural)
     →   List/build

Prelude/Natural/even

@@ -1,3 +1,14 @@
+{-
+Returns `True` if a number if even and returns `False` otherwise
+
+Examples:
+
+```
+./even +3 = False
+
+./even +0 = True
+```
+-}
 let even : Natural → Bool
     =   Natural/even
 

Prelude/Natural/fold

@@ -1,3 +1,27 @@
+{-
+`fold` is the primitive function for consuming `Natural` numbers
+
+If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just
+replaces each `succ` and `zero` with something else
+
+Examples:
+
+```
+./fold +3 Natural (λ(x : Natural) → +5 * x) +1 = +125
+
+λ(zero : Natural) → ./fold +3 Natural (λ(x : Natural) → +5 * x) zero
+= λ(zero : Natural) → +5 * +5 * +5 * zero
+
+    λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   ./fold +3 natural succ zero
+=   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   succ (succ (succ zero))
+```
+-}
 let fold
     :   Natural
     →   ∀(natural : Type)

Prelude/Natural/isZero

@@ -1,3 +1,14 @@
+{-
+Returns `True` if a number is `+0` and returns `False` otherwise
+
+Examples:
+
+```
+./isZero +2 = False
+
+./isZero +0 = True
+```
+-}
 let isZero : Natural → Bool
     =   Natural/isZero
 

Prelude/Natural/odd

@@ -1,3 +1,13 @@
+{-
+Returns `True` if a number is odd and returns `False` otherwise
+
+Examples:
+
+```
+./odd +3 = True
+
+./odd +0 = False
+-}
 let odd : Natural → Bool
     =   Natural/odd
 

Prelude/Natural/product

@@ -1,3 +1,13 @@
+{-
+Multiply all the numbers in a `List`
+
+Examples:
+
+```
+./product ([+2, +3, +5] : List Natural) = +30
+
+./product ([] : List Natural) = +1
+-}
 let product : List Natural → Natural
     =   λ(xs : List Natural)
     →   List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) +1

Prelude/Natural/sum

@@ -1,3 +1,14 @@
+{-
+Add all the numbers in a `List`
+
+Examples:
+
+```
+./sum ([+2, +3, +5] : List Natural) = +10
+
+./sum ([] : List Natural) = +0
+```
+-}
 let sum : List Natural → Natural
     =   λ(xs : List Natural)
     →   List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) +0

Prelude/Optional/build

@@ -1,8 +1,33 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+Integer
+(   λ(optional : Type)
+→   λ(just : Integer → optional)
+→   λ(nothing : optional)
+→   just 1
+)
+= [1] : Optional Integer
+
+./build
+Integer
+(   λ(optional : Type)
+→   λ(just : Integer → optional)
+→   λ(nothing : optional)
+→   nothing
+)
+= [] : Optional Integer
+```
+-}
 let build
     :   ∀(a : Type)
     →   (   ∀(optional : Type)
         →   ∀(just : a → optional)
-        →   ∀(nothing: optional)
+        →   ∀(nothing : optional)
         →   optional
         )
     →   Optional a

Prelude/Optional/concat

@@ -1,3 +1,19 @@
+{-
+Flatten two `Optional` layers into a single `Optional` layer
+
+Examples:
+
+```
+./concat Integer ([[1] : Optional Integer] : Optional (Optional Integer))
+= [1] : Optional Integer
+
+./concat Integer ([[] : Optional Integer] : Optional (Optional Integer))
+= [] : Optional Integer
+
+./concat Integer ([] : Optional (Optional Integer))
+= [] : Optional Integer
+```
+-}
 let concat : ∀(a : Type) → Optional (Optional a) → Optional a
     =   λ(a : Type)
     →   λ(x : Optional (Optional a))

Prelude/Optional/concatMap

@@ -1,3 +1,29 @@
+{-
+This is a convenience function that combines `concat` and `map`
+
+```
+./concatMap a b f xs = ./concat b (./map a b f xs)
+```
+
+Examples:
+
+```
+./concatMap
+(List Text)
+Text
+(List/head Text)
+([["ABC", "DEF"] : List Text] : Optional (List Text))
+= ["ABC"] : Optional Text
+
+./concatMap
+(List Text)
+Text
+(List/head Text)
+([[] : List Text] : Optional (List Text))
+= [] : Optional Text
+```
+
+-}
 let concatMap
     : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → Optional a → Optional b
     =   λ(a : Type)

Prelude/Optional/fold

@@ -1,3 +1,14 @@
+{-
+`fold` is the primitive function for consuming `Optional` values
+
+Examples:
+
+```
+./fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2
+
+./fold Integer ([]  : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0
+```
+-}
 let fold
     :   ∀(a : Type)
     →   Optional a

Prelude/Optional/head

@@ -1,3 +1,25 @@
+{-
+Returns the first non-empty `Optional` value in a `List`
+
+Examples:
+
+```
+./head
+Integer
+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]
+    : List (Optional Integer)
+)
+= [1] : Optional Integer
+
+./head
+Integer
+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))
+= [] : Optional Integer
+
+./head Integer ([] : List (Optional Integer))
+= [] : Optional Integer
+```
+-}
 let head : ∀(a : Type) → List (Optional a) → Optional a
     =   λ(a : Type)
     →   λ(xs : List (Optional a))

Prelude/Optional/last

@@ -1,3 +1,25 @@
+{-
+Returns the last non-empty `Optional` value in a `List`
+
+Examples:
+
+```
+./last
+Integer
+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]
+    : List (Optional Integer)
+)
+= [2] : Optional Integer
+
+./last
+Integer
+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))
+= [] : Optional Integer
+
+./last Integer ([] : List (Optional Integer))
+= [] : Optional Integer
+```
+-}
 let last : ∀(a : Type) → List (Optional a) → Optional a
     =   λ(a : Type)
     →   λ(xs : List (Optional a))

Prelude/Optional/length

@@ -1,6 +1,17 @@
+{-
+Returns `+1` if the `Optional` value is present and `+0` if absent
+
+Examples:
+
+```
+./length Integer ([3] : Optional Integer) = +1
+
+./length Integer ([] : Optional Integer) = +0
+```
+-}
 let length : ∀(a : Type) → Optional a → Natural
     =   λ(a : Type)
     →   λ(xs : Optional a)
-    →   Optional/fold a xs Natural (λ(x : a) → +1) +0
+    →   Optional/fold a xs Natural (λ(_ : a) → +1) +0
 
 in  length

Prelude/Optional/map

@@ -1,3 +1,16 @@
+{-
+Transform an `Optional` value with a function
+
+Examples:
+
+```
+./map Natural Bool Natural/even ([+3] : Optional Natural)
+= [False] : Optional Bool
+
+./map Natural Bool Natural/even ([] : Optional Natural)
+= [] : Optional Bool
+```
+-}
 let map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b
     =   λ(a : Type)
     →   λ(b : Type)

Prelude/Text/concat

@@ -1,3 +1,14 @@
+{-
+Concatenate all the `Text` values in a `List`
+
+Examples:
+
+```
+./concat (["ABC", "DEF", "GHI"] : List Text) = "ABCDEFGHI"
+
+./concat ([] : List Text) = ""
+```
+-}
 let concat : List Text → Text
     =   λ(xs : List Text)
     →   List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) ""