git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2054 from bmastenbrook/patch-1
a87a66bEdwin Brady
docs/proofs/patterns.rst+4−3
compare with master
unifiedsplit
@@ -184,7 +184,8 @@ Again, the ``fromInteger 0`` is merely due to ``Nat`` being an instance
184of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do
184of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do
185we use this to update the goal to ``S k = S k``?
185we use this to update the goal to ``S k = S k``?
186
186
187−To achieve this, provides a ``replace`` function as part of the prelude:
187+To achieve this, Idris provides a ``replace`` function as part of the
188+prelude:
188
189
189.. code-block:: idris
190.. code-block:: idris
190
191
@@ -195,8 +196,8 @@ Given a proof that ``x = y``, and a property ``P`` which holds for
195``x``, we can get a proof of the same property for ``y``, because we
196``x``, we can get a proof of the same property for ``y``, because we
196know ``x`` and ``y`` must be the same. In practice, this function can be
197know ``x`` and ``y`` must be the same. In practice, this function can be
197a little tricky to use because in general the implicit argument ``P``
198a little tricky to use because in general the implicit argument ``P``
198−can be hard to infer by unification, so provides a high level syntax
199+can be hard to infer by unification, so Idris provides a high level
199−which calculates the property and applies replace:
200+syntax which calculates the property and applies ``replace``:
200
201
201.. code-block:: idris
202.. code-block:: idris
202
203
docs/proofs/pluscomm.rst+2−2
@@ -132,7 +132,7 @@ equalities between values in different types:
132
132
133 idris_not_php : 2 = "2"
133 idris_not_php : 2 = "2"
134
134
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.
181
181
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