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