Add support for dependent types

Prelude/Bool/and

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

Prelude/Bool/build

@@ -1,17 +1,18 @@
 {-
 `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
 
+let example0 =
+        assert
+      : build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) ≡ True
+
+let example1 =
+        assert
+      :   build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)
+        ≡ False
+
 in  build

Prelude/Bool/even

@@ -1,22 +1,18 @@
 {-
 Returns `True` if there are an even number of `False` elements in the list and
 returns `False` otherwise
-
-Examples:
-
-```
-./even [ False, True, False ] = True
-
-./even [ False, True ] = False
-
-./even [ False ] = False
-
-./even ([] : List Bool) = True
-```
 -}
 let even
     : List Bool → Bool
     =   λ(xs : List Bool)
       → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
 
+let example0 = assert : even [ False, True, False ] ≡ True
+
+let example1 = assert : even [ False, True ] ≡ False
+
+let example2 = assert : even [ False ] ≡ False
+
+let example3 = assert : even ([] : List Bool) ≡ True
+
 in  even

Prelude/Bool/fold

@@ -1,13 +1,5 @@
 {-
 `fold` is essentially the same as `if`/`then`/else` except as a function
-
-Examples:
-
-```
-./fold True Natural 0 1 = 0
-
-./fold False Natural 0 1 = 1
-```
 -}
 let fold
     : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
@@ -17,4 +9,8 @@ let fold
       → λ(false : bool)
       → if b then true else false
 
+let example0 = assert : fold True Natural 0 1 ≡ 0
+
+let example1 = assert : fold False Natural 0 1 ≡ 1
+
 in  fold

Prelude/Bool/not

@@ -1,12 +1,10 @@
 {-
 Flip the value of a `Bool`
+-}
+let not : Bool → Bool = λ(b : Bool) → b == False
 
-Examples:
+let example0 = assert : not True ≡ False
 
-```
-./not True = False
+let example1 = assert : not False ≡ True
 
-./not False = True
-```
--}
-let not : Bool → Bool = λ(b : Bool) → b == False in not
+in  not

Prelude/Bool/odd

@@ -1,22 +1,18 @@
 {-
 Returns `True` if there are an odd number of `True` elements in the list and
 returns `False` otherwise
-
-Examples:
-
-```
-./odd [ True, False, True ] = False
-
-./odd [ True, False ] = True
-
-./odd [ True ] = True
-
-./odd ([] : List Bool) = False
-```
 -}
 let odd
     : List Bool → Bool
     =   λ(xs : List Bool)
       → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
 
+let example0 = assert : odd [ True, False, True ] ≡ False
+
+let example1 = assert : odd [ True, False ] ≡ True
+
+let example2 = assert : odd [ True ] ≡ True
+
+let example3 = assert : odd ([] : List Bool) ≡ False
+
 in  odd

Prelude/Bool/or

@@ -1,18 +1,14 @@
 {-
 The `or` function returns `True` if there are any `True` elements in the `List`
 and returns `False` otherwise
-
-Examples:
-
-```
-./or [ True, False, True ] = 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
 
+let example0 = assert : or [ True, False, True ] ≡ True
+
+let example1 = assert : or ([] : List Bool) ≡ False
+
 in  or

Prelude/Bool/show

@@ -1,13 +1,11 @@
 {-
 Render a `Bool` as `Text` using the same representation as Dhall source code
 (i.e. beginning with a capital letter)
+-}
+let show : Bool → Text = λ(b : Bool) → if b then "True" else "False"
 
-Examples:
+let example0 = assert : show True ≡ "True"
 
-```
-./show True  = "True"
+let example1 = assert : show False ≡ "False"
 
-./show False = "False"
-```
--}
-let show : Bool → Text = λ(b : Bool) → if b then "True" else "False" in show
+in  show

Prelude/Double/show

@@ -1,13 +1,11 @@
 {-
 Render a `Double` as `Text` using the same representation as Dhall source
 code (i.e. a decimal floating point number with a leading `-` sign if negative)
+-}
+let show : Double → Text = Double/show
 
-Examples:
+let example0 = assert : show -3.1 ≡ "-3.1"
 
-```
-./show -3.1 = "-3.1"
+let example1 = assert : show 0.4 ≡ "0.4"
 
-./show  0.4 =  "0.4"
-```
--}
-let show : Double → Text = Double/show in show
+in  show

Prelude/Function/compose

@@ -1,12 +1,5 @@
 {-
 Compose two functions into one.
-
-Examples:
-
-```
-./compose Natural Natural Bool (λ(n : Natural) → n + n) ../Natural/even 3
-= True
-```
 -}
 let compose
     : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
@@ -18,4 +11,9 @@ let compose
       → λ(x : A)
       → g (f x)
 
+let example0 =
+        assert
+      :   compose Natural Natural Bool (λ(n : Natural) → n + n) Natural/even 3
+        ≡ True
+
 in  compose

Prelude/Integer/show

@@ -2,13 +2,11 @@
 Render an `Integer` as `Text` using the same representation as Dhall source
 code (i.e. a decimal number with a leading `-` sign if negative and a leading
 `+` sign if non-negative)
+-}
+let show : Integer → Text = Integer/show
 
-Examples:
+let example0 = assert : show -3 ≡ "-3"
 
-```
-./show -3 = "-3"
+let example1 = assert : show +0 ≡ "+0"
 
-./show +0 = "+0"
-```
--}
-let show : Integer → Text = Integer/show in show
+in  show

Prelude/Integer/toDouble

@@ -1,12 +1,10 @@
 {-
 Convert an `Integer` to the corresponding `Double`
+-}
+let toDouble : Integer → Double = Integer/toDouble
 
-Examples:
+let example0 = assert : toDouble -3 ≡ -3.0
 
-```
-./toDouble -3 = -3.0
+let example1 = assert : toDouble +2 ≡ 2.0
 
-./toDouble +2 = 2.0
-```
--}
-let toDouble : Integer → Double = Integer/toDouble in toDouble
+in  toDouble

Prelude/JSON/keyText

@@ -1,17 +1,14 @@
 {-
 Builds a key-value record such that a List of them will be converted to a
 homogeneous record by dhall-to-json and dhall-to-yaml.
+
 Both key and value are fixed to Text.
 Take a look at `Record/keyValue` for a polymorphic version.
-
-Example:
-
-```
-./keyText "foo" "bar" = { mapKey = "foo", mapValue = "bar" }
-```
 -}
-
 let keyText =
       λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
 
+let example0 =
+      assert : keyText "foo" "bar" ≡ { mapKey = "foo", mapValue = "bar" }
+
 in  keyText

Prelude/JSON/keyValue

@@ -1,20 +1,17 @@
 {-
 Builds a key-value record such that a List of them will be converted to a
 homogeneous record by dhall-to-json and dhall-to-yaml.
-
-Examples:
-
-```
-./keyValue Natural "foo" 2 = { mapKey = "foo", mapValue = 2 }
-
-./keyValue Text "bar" "baz" = { mapKey = "bar", mapValue = "baz" }
-```
 -}
-
 let keyValue =
         λ(v : Type)
       → λ(key : Text)
       → λ(value : v)
       → { mapKey = key, mapValue = value }
 
+let example0 =
+      assert : keyValue Natural "foo" 2 ≡ { mapKey = "foo", mapValue = 2 }
+
+let example1 =
+      assert : keyValue Text "bar" "baz" ≡ { mapKey = "bar", mapValue = "baz" }
+
 in  keyValue

Prelude/List/all

@@ -1,14 +1,6 @@
 {-
 Returns `True` if the supplied function returns `True` for all elements in the
 `List`
-
-Examples:
-
-```
-./all Natural Natural/even [ 2, 3, 5 ] = False
-
-./all Natural Natural/even ([] : List Natural) = True
-```
 -}
 let all
     : ∀(a : Type) → (a → Bool) → List a → Bool
@@ -17,4 +9,8 @@ let all
       → λ(xs : List a)
       → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True
 
+let example0 = assert : all Natural Natural/even [ 2, 3, 5 ] ≡ False
+
+let example1 = assert : all Natural Natural/even ([] : List Natural) ≡ True
+
 in  all

Prelude/List/any

@@ -1,14 +1,6 @@
 {-
 Returns `True` if the supplied function returns `True` for any element in the
 `List`
-
-Examples:
-
-```
-./any Natural Natural/even [ 2, 3, 5 ] = True
-
-./any Natural Natural/even ([] : List Natural) = False
-```
 -}
 let any
     : ∀(a : Type) → (a → Bool) → List a → Bool
@@ -17,4 +9,8 @@ let any
       → λ(xs : List a)
       → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
 
+let example0 = assert : any Natural Natural/even [ 2, 3, 5 ] ≡ True
+
+let example1 = assert : any Natural Natural/even ([] : List Natural) ≡ False
+
 in  any