@@ -130,8 +130,8 @@ We can have a type which corresponds to disjunction:
130.. code-block:: idris
130.. code-block:: idris
132 data Or : Type -> Type -> Type where
132 data Or : Type -> Type -> Type where
133− OrIntroLeft : a -> A a b
133+ OrIntroLeft : a -> A a b
134− OrIntroRight : b -> A a b
134+ OrIntroRight : b -> A a b
136There is a built in type called 'Either'.
136There is a built in type called 'Either'.
@@ -219,7 +219,7 @@ These are axioms, that is a propositions/types that are asserted to be true with
220.. code-block:: idris
220.. code-block:: idris
222− commutePlus ``postulate``: x -> y -> plus x y = plus y x
222+ postulate commutePlus: (x:Nat) -> (y:Nat) -> plus x y = plus y x
224Alternatively 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.
224Alternatively 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.