Merge pull request #2451 from cantora/imports-in-interp-example
make light of `Data.Vect` and `Data.Fin` imports in the interp example
commit91a8cc4e992de622fdf17eae6556de0ab601e5cd
authorDavid Christiansen <david@davidchristiansen.dk>
dateWed 22 Jul 2015, 10:49 (11 years ago)
parentf605128f236bff
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.