@@ -578,16 +578,17 @@ this simply by updating the type of ``eval`` to include ``STDIO``.
579 eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]
579 eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]
581−Note that using ``STDIO`` will restrict the number of contexts in
581+.. note:: Using ``STDIO`` will restrict the number of contexts in
582−which ``eval`` can be ``run`` to those which support ``STDIO``, such
582+ which ``eval`` can be ``run`` to those which support
583−as ``IO``. Once effect lists get longer, it can be a good idea instead
583+ ``STDIO``, such as ``IO``. Once effect lists get longer, it
584+ can be a good idea instead to encapsulate sets of effects in
584−to encapsulate sets of effects in a type synonym. This is achieved as
585+ a type synonym. This is achieved as follows, simply by
585−follows, simply by defining a function which computes a type, since
586+ defining a function which computes a type, since types are
586−types are first class in Idris:
587+ first class in Idris:
588−.. code-block:: idris
589+ .. code-block:: idris
590− EvalEff : Type -> Type
591+ EvalEff : Type -> Type
591− EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]
592+ EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]
593− eval : Expr -> EvalEff Integer
594+ eval : Expr -> EvalEff Integer