@@ -68,6 +68,15 @@ The full representation of expressions is:
68 Lazy (Expr G a) ->
68 Lazy (Expr G a) ->
69 Lazy (Expr G a) -> Expr G a
69 Lazy (Expr G a) -> Expr G a
71+The code above makes use of the ``Vect`` and ``Fin`` types from the
72+Idris standard library. We import them because they are not provided
71Since expressions are indexed by their type, we can read the typing
80Since expressions are indexed by their type, we can read the typing
72rules of the language from the definitions of the constructors. Let us
81rules of the language from the definitions of the constructors. Let us
73look at each constructor in turn.
82look at each constructor in turn.