Fix typo
commit242e1039629a163cbdb5798aa5677493e615c802
authorJunior Rojas <jrojasdavalos@gmail.com>
dateSat 3 Feb 2018, 06:33 (9 years ago)
parenta7ad4e6
docs/reference/erasure.rst+1−1
@@ -103,7 +103,7 @@ that's a moot point for two reasons:
103103
104104This ought not to be the case since the ``Nat`` are never used at
105105runtime and they are only there for typechecking purposes. Hence we
106−should get rid of them and get runtime code similar to what a idris
106+should get rid of them and get runtime code similar to what an Idris
107107programmer would write.
108108
109109U-views of lists