@@ -99,11 +99,11 @@ So now that we can represent propositions as types other aspects of propositiona
9999+----------+-------------------+--------------------------+
100100| B | y=z | |
101101+----------+-------------------+--------------------------+
102−| and | A /\ B | Pair(x=y,y=z) |
102+| and | A /\\ B | ``Pair(x=y,y=z)`` |
103103+----------+-------------------+--------------------------+
104−| or | A \/ B | Either(x=y,y=z) |
104+| or | A \\/ B | ``Either(x=y,y=z)`` |
105105+----------+-------------------+--------------------------+
106−| implies | A -> B | (x=y) -> (y=x) |
106+| implies | A -> B | ``(x=y) -> (y=x)`` |
107107+----------+-------------------+--------------------------+
108108| for all | y=z | |
109109+----------+-------------------+--------------------------+
@@ -206,7 +206,7 @@ In the following pages we discuss how to resolve propositionaly equalies.
206206Axiomatic and Constructive Approaches
207207=====================================
208208
209−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:
209+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:
210210
211211- for all x,y : ``x+y=y+x``
212212- for all x: ``x + 0 = x = 0 + x``
@@ -225,7 +225,7 @@ Alternatively we could define the natural numbers based on Zero and Successor. T
225225
226226As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
227227
228−So what can we learn from this to implement out own types:
228+So what can we learn from this to implement our own types:
229229
230230- Should we try to implement both approaches?
231231- Should we define our types by constructing up from primitive types?