@@ -125,9 +125,9 @@ We can have a type which corresponds to disjunction:
125125
126126.. code-block:: idris
127127
128− data Or : Type -> Type -> Type where
129− OrIntroLeft : a -> A a b
130− OrIntroRight : b -> A a b
128+ data Or : Type -> Type -> Type where
129+ OrIntroLeft : a -> A a b
130+ OrIntroRight : b -> A a b
131131
132132There is a built in type called 'Either'.
133133
@@ -157,10 +157,10 @@ Especially when working with equalities containing variable terms (inside functi
157157
158158.. code-block:: idris
159159
160− plusReducesL : (n:Nat) -> plus Z n = n
160+ plusReducesL : (n:Nat) -> plus Z n = n
161161 plusReducesL n = Refl
162162
163− plusReducesR : (n:Nat) -> plus n Z = n
163+ plusReducesR : (n:Nat) -> plus n Z = n
164164 plusReducesR n = Refl
165165
166166plusReducesR gives the following error: