@@ -130,8 +130,8 @@ We can have a type which corresponds to disjunction:
130130.. code-block:: idris
131131
132132 data Or : Type -> Type -> Type where
133− OrIntroLeft : a -> A a b
134− OrIntroRight : b -> A a b
133+ OrIntroLeft : a -> A a b
134+ OrIntroRight : b -> A a b
135135
136136There is a built in type called 'Either'.
137137
@@ -219,7 +219,7 @@ These are axioms, that is a propositions/types that are asserted to be true with
219219
220220.. code-block:: idris
221221
222− commutePlus ``postulate``: x -> y -> plus x y = plus y x
222+ postulate commutePlus: (x:Nat) -> (y:Nat) -> plus x y = plus y x
223223
224224Alternatively we could define the natural numbers based on Zero and Successor. The axioms above then become derived rules and we also gain the ability to do inductive proofs.
225225