Fix typo
Change `and` to `an`
commit31fb7730cc4dc453d7fc05de1292288def2d6fe6
authorRichard Beddington <richard.beddington@gmail.com>
dateSun 21 Jul 2019, 09:31 (7 years ago)
parent4e70401
docs/proofs/definitional.rst+1−1
@@ -72,7 +72,7 @@ A type that is true is inhabited, that is, it can be constructed. An equality ty
7272 onePlusOne : 1+1=2
7373 onePlusOne = Refl
7474
75−So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't:
75+So how can Refl, which is a constructor without any parameters, construct an equality type? If we type it on its own then it can't:
7676
7777.. code-block:: idris
7878