@@ -103,7 +103,7 @@ that's a moot point for two reasons:
104This ought not to be the case since the ``Nat`` are never used at
104This ought not to be the case since the ``Nat`` are never used at
105runtime and they are only there for typechecking purposes. Hence we
105runtime 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
107programmer would write.
107programmer would write.
109U-views of lists
109U-views of lists