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