Merge pull request #4778 from cramsay/more_proof_doc_fixes

Additional proofs doc fixes

docs/proofs/definitional.rst

@@ -1,3 +1,7 @@
+*******************
+Background Material
+*******************
+
 In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
 
 -  Propositions and judgments
@@ -95,11 +99,11 @@ So now that we can represent propositions as types other aspects of propositiona
 +----------+-------------------+--------------------------+
 | B        | y=z               |                          |
 +----------+-------------------+--------------------------+
-| and      | A /\ B            | Pair(x=y,y=z)            |
+| and      | A /\\ B           | ``Pair(x=y,y=z)``        |
 +----------+-------------------+--------------------------+
-| or       | A \/ B            | Either(x=y,y=z)          |
+| or       | A \\/ B           | ``Either(x=y,y=z)``      |
 +----------+-------------------+--------------------------+
-| implies  | A -> B            | (x=y) -> (y=x)           |
+| implies  | A -> B            | ``(x=y) -> (y=x)``       |
 +----------+-------------------+--------------------------+
 | for all  | y=z               |                          |
 +----------+-------------------+--------------------------+
@@ -126,8 +130,8 @@ We can have a type which corresponds to disjunction:
 .. code-block:: idris
 
    data Or : Type -> Type -> Type where
-   OrIntroLeft : a -> A a b
-   OrIntroRight : b -> A a b
+     OrIntroLeft  : a -> A a b
+     OrIntroRight : b -> A a b
 
 There is a built in type called 'Either'.
 
@@ -202,7 +206,7 @@ In the following pages we discuss how to resolve propositionaly equalies.
 Axiomatic and Constructive Approaches
 =====================================
 
-How should we define types so that  we can do proofs on them? In the natural numbers with plus example we could have started by treating it as a group based on the plus operator. So we have axioms:
+How should we define types so that  we can do proofs on them? In the natural numbers with the plus example we could have started by treating it as a group based on the plus operator. So we have axioms:
 
 -  for all x,y : ``x+y=y+x``
 -  for all x: ``x + 0 = x = 0 + x``
@@ -215,13 +219,13 @@ These are axioms, that is a propositions/types that are asserted to be true with
 
 .. code-block:: idris
 
-   commutePlus ``postulate``: x -> y -> plus x y = plus y x
+   postulate commutePlus: (x:Nat) -> (y:Nat) -> plus x y = plus y x
 
 Alternatively 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.
 
 As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
 
-So what can we learn from this to implement out own types:
+So what can we learn from this to implement our own types:
 
 -  Should we try to implement both approaches?
 -  Should we define our types by constructing up from primitive types?

docs/proofs/pluscomm.rst

@@ -182,7 +182,7 @@ interface rather than using ``plus`` directly. They have the names
 
 In the remainder of this tutorial, we will explore several different
 ways of proving ``plus_commutes`` (or, to put it another way, writing
-the function.) We will also discuss how to use such equality proofs, and
+the function). We will also discuss how to use such equality proofs, and
 see where the need for them arises in practice.
 
 .. [1]

docs/proofs/propositional.rst

@@ -1,7 +1,8 @@
-This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
-
+******************************
 Proving Propositional Equality
-==============================
+******************************
+
+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
 
 We have seen that definitional equalities can be proved using ``Refl`` since they always normalise to unique values that can be compared directly.