@@ -132,7 +132,7 @@ equalities between values in different types:
133 idris_not_php : 2 = "2"
133 idris_not_php : 2 = "2"
135−Obviously, in Idris the type ``2 = 2`` is uninhabited, and one might
135+Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
136wonder why it is useful to be able to propose equalities between values
136wonder why it is useful to be able to propose equalities between values
137in different types. However, with dependent types, such equalities can
137in different types. However, with dependent types, such equalities can
138arise naturally. For example, if two vectors are equal, their lengths
138arise naturally. For example, if two vectors are equal, their lengths
@@ -177,7 +177,7 @@ given above as Idris type declarations:
177Both of these properties (and many others) are proved for natural number
177Both of these properties (and many others) are proved for natural number
178addition in the Idris standard library, using ``(+)`` from the ``Num``
178addition in the Idris standard library, using ``(+)`` from the ``Num``
179type class rather than using ``plus`` directly. They have the names
179type class rather than using ``plus`` directly. They have the names
180−``plusCommutative`` and ``plusAssociatie`` respectively.
180+``plusCommutative`` and ``plusAssociative`` respectively.
182In the remainder of this tutorial, we will explore several different
182In the remainder of this tutorial, we will explore several different
183ways of proving ``plus_commutes`` (or, to put it another way, writing
183ways of proving ``plus_commutes`` (or, to put it another way, writing