also show the other direction GetL-to-GetV
[~helmut/bidiragda.git] / Everything.agda
1 -- The sole purpose of this module is to ease compilation of everything.
2 module Everything where
3
4 import Generic
5 import FinMap
6 import CheckInsert
7 import GetTypes
8 import FreeTheorems
9 import BFF
10 import Bidir
11 import LiftGet
12 import Precond