Merge pull request #4318 from juniorrojas/patch-1
Fix typo
commit395e8a07a0a84058a66a4e618567cf431e42df9d
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateSun 4 Feb 2018, 18:52 (9 years ago)
parenta7ad4e6242e103
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