@@ -32,13 +32,14 @@ calculated just like any other value:
32 interpTy TyBool = Bool
32 interpTy TyBool = Bool
33 interpTy (TyFun A T) = interpTy A -> interpTy T
33 interpTy (TyFun A T) = interpTy A -> interpTy T
35−We’re going to define a representation of our language in such a way
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
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
37+representations of expressions by their type, **and** the types of
38−variables (the context), which we’ll be using regularly as an implicit
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
39−argument, so we define everything in a ``using`` block (keep in mind
40+represented as an implicit argument. To do so we define everything in
40−that everything after this point needs to be indented so as to be
41+a ``using`` block (keep in mind that everything after this point needs
41−inside the ``using`` block):
42+to be indented so as to be inside the ``using`` block):
43.. code-block:: idris
44.. code-block:: idris
@@ -153,7 +154,7 @@ that only the branch which is taken need be evaluated:
153Writing the Interpreter
154Writing the Interpreter
154=======================
155=======================
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,
157as well as their types. ``Env`` is an environment, indexed over the
158as well as their types. ``Env`` is an environment, indexed over the
158types in scope. Since an environment is just another form of list,
159types in scope. Since an environment is just another form of list,
159albeit with a strongly specified connection to the vector of local
160albeit with a strongly specified connection to the vector of local