@@ -65,7 +65,7 @@ is a proposition and it is also a type. This is built into Idris so when an '='
65 2 = 3 : Type
65 2 = 3 : Type
67Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.
67Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.
68−A type that is true is inhabited, that is, it can be constructed. An equality type has only on constructor 'Refl' so a proof of 1+1=2 is
68+A type that is true is inhabited, that is, it can be constructed. An equality type has only one constructor 'Refl' so a proof of 1+1=2 is
70.. code-block:: idris
70.. code-block:: idris