a87a66b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2054 from bmastenbrook/patch-1

Typo fixes for the theorem proving tutorial

commita87a66b2aa73bda3441affd14efdd6ecec2edcee authorEdwin Brady <edwin.brady@gmail.com> dateMon 23 Mar 2015, 23:59 (12 years ago) parent7d76d93 df1af5f

2 files changed+6−5

compare with master

unifiedsplit

docs/proofs/patterns.rst+4−3 docs/proofs/pluscomm.rst+2−2

docs/proofs/patterns.rst+4−3

@@ -184,7 +184,8 @@ Again, the ``fromInteger 0`` is merely due to ``Nat`` being an instance

184184of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do

185185we use this to update the goal to ``S k = S k``?

186186

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:

188189

189190.. code-block:: idris

190191

@@ -195,8 +196,8 @@ Given a proof that ``x = y``, and a property ``P`` which holds for

195196``x``, we can get a proof of the same property for ``y``, because we

196197know ``x`` and ``y`` must be the same. In practice, this function can be

197198a 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−which calculates the property and applies replace:

199+can be hard to infer by unification, so Idris provides a high level

200+syntax which calculates the property and applies ``replace``:

200201

201202.. code-block:: idris

202203

docs/proofs/pluscomm.rst+2−2

@@ -132,7 +132,7 @@ equalities between values in different types:

132132

133133 idris_not_php : 2 = "2"

134134

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

136136wonder why it is useful to be able to propose equalities between values

137137in different types. However, with dependent types, such equalities can

138138arise naturally. For example, if two vectors are equal, their lengths

@@ -177,7 +177,7 @@ given above as Idris type declarations:

177177Both of these properties (and many others) are proved for natural number

178178addition in the Idris standard library, using ``(+)`` from the ``Num``

179179type class rather than using ``plus`` directly. They have the names

180−``plusCommutative`` and ``plusAssociatie`` respectively.

180+``plusCommutative`` and ``plusAssociative`` respectively.

181181

182182In the remainder of this tutorial, we will explore several different

183183ways of proving ``plus_commutes`` (or, to put it another way, writing