turns out: ind-cong is a special case of H.congâ‚‚
[~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 Structures
6 import Instances
7 import FinMap
8 import CheckInsert
9 import GetTypes
10 import FreeTheorems
11 import BFF
12 import Bidir
13 import LiftGet
14 import Precond
15 import Examples
16 import BFFPlug