Maps: tweak whitespace

Author: yurrriq

src/Maps.lidr

@@ -1,6 +1,7 @@
 = Maps: Total and Partial Maps
 
 > module Maps
+>
 
 Maps (or dictionaries) are ubiquitous data structures both generally and in the
 theory of programming languages in particular; we're going to need them in many
@@ -52,9 +53,10 @@ equality comparison function for \idr{Id} and its fundamental property.
 
 > data Id : Type where
 >   MkId : String -> Id
-
+>
 > beq_id : (x1, x2 : Id) -> Bool
 > beq_id (MkId n1) (MkId n2) = decAsBool $ decEq n1 n2
+>
 
 \todo[inline]{Edit}
 
@@ -68,8 +70,9 @@ present purposes you can think of it as just a fancy \idr{Bool}.)
 
 > beq_id_refl : (x : Id) -> True = beq_id x x
 > beq_id_refl (MkId n) with (decEq n n)
->   beq_id_refl _ | Yes _ = Refl
+>   beq_id_refl _ | Yes _     = Refl
 >   beq_id_refl _ | No contra = absurd $ contra Refl
+>
 
 The following useful property of  \idr{beq_id} follows from an analogous lemma
 about strings:
@@ -78,8 +81,9 @@ about strings:
 
 > iff : {p,q : Type} -> Type
 > iff {p} {q} = (p -> q, q -> p)
-
+>
 > syntax [p] "<->" [q] = iff {p} {q}
+>
 
 \todo[inline]{Somehow this doesn't work if put under \idr{where} as usual}
 
@@ -106,10 +110,11 @@ for now}
 > not_true_and_false : (b = False) -> Not (b = True)
 > not_true_and_false {b=False} _ Refl impossible
 > not_true_and_false {b=True} Refl _ impossible
+>
 > not_true_is_false : Not (b = True) -> b = False
 > not_true_is_false {b=False} h = Refl
-> not_true_is_false {b=True} h = absurd $ h Refl
-
+> not_true_is_false {b=True} h  = absurd $ h Refl
+>
 > beq_id_false_iff : (beq_id x y = False) <-> Not (x = y)
 > beq_id_false_iff = (to, fro)
 > where
@@ -137,6 +142,7 @@ return a default value when we look up a key that is not present in the map.
 
 > total_map : Type -> Type
 > total_map a = Id -> a
+>
 
 Intuitively, a total map over an element type \idr{a} is just a function that
 can be used to look up \idr{Id}s, yielding \idr{a}s.
@@ -146,6 +152,7 @@ this map always returns the default element when applied to any id.
 
 > t_empty : (v : a) -> total_map a
 > t_empty v = \_ => v
+>
 
 We can also write this as:
 
@@ -159,6 +166,7 @@ More interesting is the \idr{update} function, which (as before) takes a map
 
 > t_update : (x : Id) -> (v : a) -> (m : total_map a) -> total_map a
 > t_update x v m = \x' => if beq_id x x' then v else m x'
+>
 
 This definition is a nice example of higher-order programming: \idr{t_update}
 takes a _function_ \idr{m} and yields a new function \idr{\x' => ...} that
@@ -174,21 +182,23 @@ this:
 > examplemap = t_update (MkId "foo") False $
 >              t_update (MkId "bar") True $
 >              t_empty False
+>
 
 This completes the definition of total maps. Note that we don't need to define a
 \idr{find} operation because it is just function application!
 
 > update_example1 : examplemap (MkId "baz") = False
 > update_example1 = Refl
-
+>
 > update_example2 : examplemap (MkId "foo") = False
 > update_example2 = Refl
-
+>
 > update_example3 : examplemap (MkId "quux") = False
 > update_example3 = Refl
-
+>
 > update_example4 : examplemap (MkId "bar") = True
 > update_example4 = Refl
+>
 
 To use maps in later chapters, we'll need several fundamental facts about how
 they behave. Even if you don't work the following exercises, make sure you
@@ -202,6 +212,7 @@ First, the empty map returns its default element for all keys:
 
 > t_apply_empty : t_empty v x = v
 > t_apply_empty = ?t_apply_empty_rhs
+>
 
 $\square$
 
@@ -214,6 +225,7 @@ then look up \idr{x} in the map resulting from the \idr{update}, we get back
 
 > t_update_eq : (t_update x v m) x = v
 > t_update_eq = ?t_update_eq_rhs
+>
 
 $\square$
 
@@ -226,6 +238,7 @@ a _different_ key \idr{x2} in the resulting map, we get the same result that
 
 > t_update_neq : Not (x1 = x2) -> (t_update x1 v m) x2 = m x2
 > t_update_neq neq = ?t_update_neq_rhs
+>
 
 $\square$
 
@@ -239,6 +252,7 @@ simpler map obtained by performing just the second \idr{update} on \idr{m}:
 
 > t_update_shadow : t_update x v2 $ t_update x v1 m = t_update x v2 m
 > t_update_shadow = ?t_update_shadow_rhs
+>
 
 $\square$
 
@@ -258,9 +272,10 @@ following:
 > data Reflect : Type -> Bool -> Type where
 >   ReflectT : (p : Type) -> Reflect p True
 >   ReflectF : (p : Type) -> (Not p) -> Reflect p False
-
+>
 > beq_idP : Reflect (x = y) (beq_id x y)
 > beq_idP = ?beq_idP_rhs
+>
 
 $\square$
 
@@ -279,6 +294,7 @@ the following theorem, which states that if we update a map to assign key
 
 > t_update_same : t_update x (m x) m = m
 > t_update_same = ?t_update_same_rhs
+>
 
 $\square$
 
@@ -292,6 +308,7 @@ we do the updates.
 > t_update_permute : Not (x2 = x1) -> t_update x1 v1 $ t_update x2 v2 m
 >                                   = t_update x2 v2 $ t_update x1 v1 m
 > t_update_permute neq = ?t_update_permute_rhs
+>
 
 $\square$
 
@@ -304,40 +321,41 @@ a} and default element \idr{Nothing}.
 
 > partial_map : Type -> Type
 > partial_map a = total_map (Maybe a)
-
+>
 > empty : partial_map a
 > empty = t_empty Nothing
-
+>
 > update : (x : Id) -> (v : a) -> (m : partial_map a) -> partial_map a
 > update x v m = t_update x (Just v) m
+>
 
 We now straightforwardly lift all of the basic lemmas about total maps to
 partial maps.
 
 > apply_empty : empty {a} x = Nothing {a}
 > apply_empty = Refl
-
+>
 > update_eq : (update x v m) x = Just v
 > update_eq {x} {v} {m} =
 >   rewrite t_update_eq {x} {v=Just v} {m} in
->   Refl
-
+>           Refl
+>
 > update_neq : Not (x2 = x1) -> (update x2 v m) x1 = m x1
 > update_neq {x1} {x2} {v} {m} neq =
 >   rewrite t_update_neq neq {x1=x2} {x2=x1} {v=Just v} {m} in
->   Refl
-
+>           Refl
+>
 > update_shadow : update x v2 $ update x v1 m = update x v2 m
 > update_shadow {x} {v1} {v2} {m} =
 >   rewrite t_update_shadow {x} {v1=Just v1} {v2=Just v2} {m} in
->   Refl
-
+>           Refl
+>
 > update_same : m x = Just v -> update x v m = m
 > update_same {x} {m} {v} prf =
 >   rewrite sym prf in
 >   rewrite t_update_same {x} {m} in
->   Refl
-
+>           Refl
+>
 > update_permute : Not (x2 = x1) -> update x1 v1 $ update x2 v2 m
 >                                 = update x2 v2 $ update x1 v1 m
 > update_permute {x1} {x2} {v1} {v2} {m} neq =