@@ -99,11 +99,11 @@ So now that we can represent propositions as types other aspects of propositiona
99+----------+-------------------+--------------------------+
99+----------+-------------------+--------------------------+
100| B | y=z | |
100| B | y=z | |
101+----------+-------------------+--------------------------+
101+----------+-------------------+--------------------------+
102−| and | A /\ B | Pair(x=y,y=z) |
102+| and | A /\\ B | ``Pair(x=y,y=z)`` |
103+----------+-------------------+--------------------------+
103+----------+-------------------+--------------------------+
104−| or | A \/ B | Either(x=y,y=z) |
104+| or | A \\/ B | ``Either(x=y,y=z)`` |
105+----------+-------------------+--------------------------+
105+----------+-------------------+--------------------------+
106−| implies | A -> B | (x=y) -> (y=x) |
106+| implies | A -> B | ``(x=y) -> (y=x)`` |
107+----------+-------------------+--------------------------+
107+----------+-------------------+--------------------------+
108| for all | y=z | |
108| for all | y=z | |
109+----------+-------------------+--------------------------+
109+----------+-------------------+--------------------------+
@@ -206,7 +206,7 @@ In the following pages we discuss how to resolve propositionaly equalies.
206Axiomatic and Constructive Approaches
206Axiomatic and Constructive Approaches
207=====================================
207=====================================
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:
211- for all x,y : ``x+y=y+x``
211- for all x,y : ``x+y=y+x``
212- for all x: ``x + 0 = x = 0 + x``
212- 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
226As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
226As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
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:
230- Should we try to implement both approaches?
230- Should we try to implement both approaches?
231- Should we define our types by constructing up from primitive types?
231- Should we define our types by constructing up from primitive types?