@@ -36,7 +36,9 @@ We’re going to define a representation of our language in such a way
36that only well-typed programs can be represented. We’ll index the
36that only well-typed programs can be represented. We’ll index the
37representations of expressions by their type and the types of local
37representations of expressions by their type and the types of local
38variables (the context), which we’ll be using regularly as an implicit
38variables (the context), which we’ll be using regularly as an implicit
39−argument, so we define everything in a ``using`` block:
39+argument, so we define everything in a ``using`` block (keep in mind
40+that everything after this point needs to be indented so as to be
41+inside the ``using`` block):
41.. code-block:: idris
43.. code-block:: idris