module everything where

-- We import everything so that html is generated for all files, even
-- those that are alternatives, when with compile with --html.
--
-- Hence this file should be imported in the top file, namely
-- Examples.agda.


import Addition
import Cantor
import Choice
import DataStructures
import Equality
import Finite
import Finite-JK-Shifts
import FinitePigeon
import InfinitePigeon
import InfinitePigeon2011-05-12
import InfinitePigeonLessEfficient
import InfinitePigeonOriginal
import J-AC-N
import J-DC
import J-Shift
import J-Shift-BBC
import J-Shift-Selection
import JK-LogicalFacts
import JK-Monads
import K-AC-N
import K-DC
import K-Shift
import K-Shift-BBC
import K-Shift-MBR
import K-Shift-Selection
import K-Shift-from-J-Shift
import Logic
import LogicalFacts
import Naturals
import Order
import PigeonProgram
import Two