@@ -212,19 +212,21 @@ keyword.
212 codata Stream : Type -> Type where
212 codata Stream : Type -> Type where
213 (::) a -> Stream a -> Stream a
213 (::) a -> Stream a -> Stream a
215−This is syntactic sugar for
215+This is syntactic sugar for the following, which is usually preferred:
217.. code:: idris
217.. code:: idris
219 data Stream : Type -> Type where
219 data Stream : Type -> Type where
220− (::) a -> Delayed Infinite (Stream a) -> Stream a
220+ (::) a -> Inf (Stream a) -> Stream a
222−Every occurence of the the defined type in a constructor argument will
222+Every occurence of the the defined type in a constructor argument will be
223−be wrapped in the ``Delayed Infinite`` type constructor. This has the
223+wrapped in the ``Inf`` type constructor. This has the effect of delaying the
224−effect of delaying the evaluation of the second argument when the data
224+evaluation of the second argument when the data constructor is applied.
225−constructor is applied. The argument is only evaluated when we pattern
225+An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
226−match against the constructor.
226+implicitly) adn evaluated using ``Force`` (again inserted implicitly).
228+Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
229+to pass the totality checker.