make light of `Data.Vect` and `Data.Fin` imports in the interp example
the interp documentation section assumes that these types are in the
prelude.
commitf236bfffa3ae7fb13787f085815b565fef8e4ae0
authoranthony cantor <cantora@gubbi.mobi>
dateSun 19 Jul 2015, 15:06 (11 years ago)
parent8518aa3
docs/tutorial/interp.rst+9
@@ -68,6 +68,15 @@ The full representation of expressions is:
6868 Lazy (Expr G a) ->
6969 Lazy (Expr G a) -> Expr G a
7070
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
73+in the prelude:
74+
75+.. code-block:: idris
76+
77+ import Data.Vect
78+ import Data.Fin
79+
7180Since expressions are indexed by their type, we can read the typing
7281rules of the language from the definitions of the constructors. Let us
7382look at each constructor in turn.