@@ -32,13 +32,14 @@ calculated just like any other value:
3232 interpTy TyBool = Bool
3333 interpTy (TyFun A T) = interpTy A -> interpTy T
3434
35−We’re going to define a representation of our language in such a way
36−that only well-typed programs can be represented. We’ll index the
37−representations of expressions by their type and the types of local
38−variables (the context), which we’ll be using regularly as an implicit
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):
35+We're going to define a representation of our language in such a way
36+that only well-typed programs can be represented. We'll index the
37+representations of expressions by their type, **and** the types of
38+local variables (the context). The context can be represented using
39+the ``Vect`` data type, and as it will be used regularly it will be
40+represented as an implicit argument. To do so we define everything in
41+a ``using`` block (keep in mind that everything after this point needs
42+to be indented so as to be inside the ``using`` block):
4243
4344.. code-block:: idris
4445
@@ -153,7 +154,7 @@ that only the branch which is taken need be evaluated:
153154Writing the Interpreter
154155=======================
155156
156−When we evaluate an ``Expr``, we’ll need to know the values in scope,
157+When we evaluate an ``Expr``, we'll need to know the values in scope,
157158as well as their types. ``Env`` is an environment, indexed over the
158159types in scope. Since an environment is just another form of list,
159160albeit with a strongly specified connection to the vector of local