Lists: normalize whitespace

Author: yurrriq

src/Lists.lidr

@@ -8,6 +8,7 @@
 
 > %default total
 
+
 == Pairs of Numbers
 
 In an inductive type definition, each constructor can take any number of
@@ -94,20 +95,23 @@ match in `fst` and `snd`. We can do this with `case`.
 Notice that `case` matches just one pattern here. That's because `NatProd`s can
 only be constructed in one way.
 
+
 === Exercise: 1 star (snd_fst_is_swap)
 
 > snd_fst_is_swap : (p : NatProd) -> (snd p, fst p) = swap_pair p
 > snd_fst_is_swap p = ?snd_fst_is_swap_rhs
 
 $\square$
 
+
 === Exercise: 1 star, optional (fst_swap_is_snd)
 
 > fst_swap_is_snd : (p : NatProd) -> fst (swap_pair p) = snd p
 > fst_swap_is_snd p = ?fst_swap_is_snd_rhs
 
 $\square$
 
+
 == Lists of Numbers
 
 Generalizing the definition of pairs, we can describe the type of _lists_ of
@@ -168,6 +172,7 @@ square-bracket notation for lists; the right-hand side of the third one
 illustrates Coq's syntax for declaring n-ary notations and translating them to
 nested sequences of binary constructors.
 
+
 === Repeat
 
 A number of functions are useful for manipulating lists. For example, the
@@ -178,6 +183,7 @@ A number of functions are useful for manipulating lists. For example, the
 > repeat n Z = Nil
 > repeat n (S k) = n :: repeat n k
 
+
 === Length
 
 The `length` function calculates the length of a list.
@@ -186,6 +192,7 @@ The `length` function calculates the length of a list.
 > length Nil = Z
 > length (h :: t) = S (length t)
 
+
 === Append
 
 The `app` function concatenates (appends) two lists.
@@ -208,6 +215,7 @@ convenient to have an infix operator for it.
 > test_app3 : ((1::2::3::[]) ++ []) = (1::2::3::[])
 > test_app3 = Refl
 
+
 === Head (with default) and Tail
 
 Here are two smaller examples of programming with lists. The `hd` function
@@ -232,6 +240,7 @@ first element, so we must pass a default value to be returned in that case.
 > test_tl : tl (1::2::3::[]) = (2::3::[])
 > test_tl = Refl
 
+
 === Exercises
 
 ==== Exercise: 2 stars, recommended (list_funs)
@@ -259,6 +268,7 @@ below. Have a look at the tests to understand what these functions should do.
 
 $\square$
 
+
 ==== Exercise: 3 stars, advanced (alternate)
 
 Complete the definition of `alternate`, which "zips up" two lists into one,
@@ -289,6 +299,7 @@ requires defining a new kind of pairs, but this is not the only way.)
 
 $\square$
 
+
 === Bags via Lists
 
 A `bag` (or `multiset`) is like a set, except that each element can appear
@@ -298,6 +309,7 @@ represent a bag of numbers as a list.
 > Bag : Type
 > Bag = NatList
 
+
 ==== Exercise: 3 stars, recommended (bag_functions)
 
 Complete the following definitions for the functions `count`, `sum`, `add`, and
@@ -352,6 +364,7 @@ functions that have already been defined.
 
 $\square$
 
+
 ==== Exercise: 3 stars, optional (bag_more_functions)
 
 Here are some more bag functions for you to practice with.
@@ -386,7 +399,7 @@ return the same bag unchanged.
 > test_remove_all3 : count 4 (remove_all 5 (2::1::5::4::1::4::[])) = 2
 > test_remove_all3 = ?test_remove_all3_rhs
 
-> test_remove_all4 : count 5 
+> test_remove_all4 : count 5
 >                    (remove_all 5 (2::1::5::4::5::1::4::5::1::4::[])) = 0
 > test_remove_all4 = ?test_remove_all4_rhs
 
@@ -401,6 +414,7 @@ return the same bag unchanged.
 
 $\square$
 
+
 ==== Exercise: 3 stars, recommended (bag_theorem)
 
 Write down an interesting theorem `bag_theorem` about bags involving the
@@ -413,6 +427,7 @@ ask for help if you get stuck!
 
 $\square$
 
+
 == Reasoning About Lists
 
 As with numbers, simple facts about list-processing functions can sometimes be
@@ -441,13 +456,15 @@ tail of the list it is constructing).
 Usually, though, interesting theorems about lists require induction for their
 proofs.
 
+
 ==== Micro-Sermon
 
 Simply reading example proof scripts will not get you very far! It is important
 to work through the details of each one, using Idris and thinking about what
 each step achieves. Otherwise it is more or less guaranteed that the exercises
 will make no sense when you get to them. 'Nuff said.
 
+
 === Induction on Lists
 
 Proofs by induction over datatypes like `NatList` are a little less familiar
@@ -512,6 +529,7 @@ _Proof_: By induction on `l1`.
     `n :: ((l1' ++ l2) ++ l 3) = n :: (l1' ++ (l2 ++ l3))`,
     which is immediate from the induction hypothesis. $\square$
 
+
 ==== Reversing a List
 
 For a slightly more involved example of inductive proof over lists, suppose we
@@ -527,6 +545,7 @@ use `app` to define a list-reversing function `rev`:
 > test_rev2 : rev Nil = Nil
 > test_rev2 = Refl
 
+
 ==== Properties of rev
 
 Now let's prove some theorems about our newly defined `rev`. For something a bit
@@ -583,7 +602,7 @@ _Proof_: By induction on `l1`.
 
   - First, suppose `l1 = []`. We must show
     `length ([] ++ l2) = length [] + length l2`,
-    which follows directly from the definitions of `length` and `++`.  
+    which follows directly from the definitions of `length` and `++`.
 
   - Next, suppose `l1 = n :: l1'`, with
     `length (l1' ++ l2) = length l1' + length l2`.
@@ -650,6 +669,7 @@ the book; it can save you a lot of time!
 If you are using ProofGeneral, you can run Search with C-c C-a C-a. Pasting its
 response into your buffer can be accomplished with C-c C-;.
 
+
 === List Exercises, Part 1
 
 ==== Exercise: 3 stars (list_exercises)
@@ -680,6 +700,7 @@ An exercise about your implementation of `nonzeros`:
 
 $\square$
 
+
 ==== Exercise: 2 stars (beq_NatList)
 
 Fill in the definition of `beq_NatList`, which compares lists of numbers for
@@ -702,6 +723,7 @@ equality. Prove that `beq_NatList l l` yields `True` for every list `l`.
 
 $\square$
 
+
 === List Exercises, Part 2
 
 ==== Exercise: 3 stars, advanced (bag_proofs)
@@ -726,6 +748,7 @@ The following lemma about `leb` might help you in the next proof.
 
 $\square$
 
+
 ==== Exercise: 3 stars, optional (bag_count_sum)
 
 Write down an interesting theorem `bag_count_sum` about bags involving the
@@ -736,6 +759,7 @@ the proof depends on how you defined `count`!)
 
 $\square$
 
+
 ==== Exercise: 4 stars, advanced (rev_injective)
 
 Prove that the `rev` function is injective -- that is,
@@ -747,6 +771,7 @@ Prove that the `rev` function is injective -- that is,
 
 $\square$
 
+
 == Options
 
 Suppose we want to write a function that returns the `n`th element of some list.
@@ -811,6 +836,7 @@ default in the `None` case.
 > option_elim d (Some k) = k
 > option_elim d None = d
 
+
 ==== Exercise: 2 stars (hd_error)
 
 Using the same idea, fix the `hd` function from earlier so we don't have to pass
@@ -830,6 +856,7 @@ a default element for the `Nil` case.
 
 $\square$
 
+
 ==== Exercise: 1 star, optional (option_elim_hd)
 
 This exercise relates your new `hd_error` to the old `hd`.
@@ -840,6 +867,7 @@ This exercise relates your new `hd_error` to the old `hd`.
 
 $\square$
 
+
 == Partial Maps
 
 As a final illustration of how data structures can be defined in Idris, here is
@@ -861,6 +889,7 @@ We'll also need an equality test for `Id`s:
 > beq_id : (x1, x2 : Id) -> Bool
 > beq_id (MkId n1) (MkId n2) = beq_nat n1 n2
 
+
 ==== Exercise: 1 star (beq_id_refl)
 
 > beq_id_refl : (x : Id) -> True = beq_id x x
@@ -898,6 +927,7 @@ first one it encounters.
 >                              then Some v
 >                              else find x d'
 
+
 ==== Exercise: 1 star (update_eq)
 
 >   update_eq : (d : PartialMap) -> (x : Id) -> (v : Nat) ->
@@ -906,6 +936,7 @@ first one it encounters.
 
 $\square$
 
+
 ==== Exercise: 1 star (update_neq)
 
 >   update_neq : (d : PartialMap) -> (x, y : Id ) -> (o : Nat) ->
@@ -915,6 +946,7 @@ $\square$
 
 $\square$
 
+
 ==== Exercise: 2 stars (baz_num_elts)
 
 Consider the following inductive definition:
@@ -926,4 +958,4 @@ Consider the following inductive definition:
 How _many_ elements does the type `Baz` have? (Answer in English or the natural
 language of your choice.)
 
-$\square$
+$\square$