@@ -125,9 +125,9 @@ We can have a type which corresponds to disjunction:
126.. code-block:: idris
126.. code-block:: idris
128− data Or : Type -> Type -> Type where
128+ data Or : Type -> Type -> Type where
129− OrIntroLeft : a -> A a b
129+ OrIntroLeft : a -> A a b
130− OrIntroRight : b -> A a b
130+ OrIntroRight : b -> A a b
132There is a built in type called 'Either'.
132There is a built in type called 'Either'.
@@ -157,10 +157,10 @@ Especially when working with equalities containing variable terms (inside functi
158.. code-block:: idris
158.. code-block:: idris
160− plusReducesL : (n:Nat) -> plus Z n = n
160+ plusReducesL : (n:Nat) -> plus Z n = n
161 plusReducesL n = Refl
161 plusReducesL n = Refl
163− plusReducesR : (n:Nat) -> plus n Z = n
163+ plusReducesR : (n:Nat) -> plus n Z = n
164 plusReducesR n = Refl
164 plusReducesR n = Refl
166plusReducesR gives the following error:
166plusReducesR gives the following error: