@@ -223,7 +223,7 @@ Every occurence of the the defined type in a constructor argument will be
223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
224evaluation of the second argument when the data constructor is applied.
224evaluation of the second argument when the data constructor is applied.
225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
226−implicitly) adn evaluated using ``Force`` (again inserted implicitly).
226+implicitly) and evaluated using ``Force`` (again inserted implicitly).
228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
229to pass the totality checker.
229to pass the totality checker.