summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Everything.agda25
-rw-r--r--cfe-proof.agda-lib4
2 files changed, 29 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..d4a2662
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,25 @@
+module Everything where
+
+import Cfe.Context
+import Cfe.Context.Base
+import Cfe.Context.Properties
+import Cfe.Derivation
+import Cfe.Derivation.Base
+import Cfe.Derivation.Properties
+import Cfe.Expression
+import Cfe.Expression.Base
+import Cfe.Expression.Properties
+import Cfe.Fin
+import Cfe.Fin.Base
+import Cfe.Fin.Properties
+import Cfe.Judgement
+import Cfe.Judgement.Base
+import Cfe.Judgement.Properties
+import Cfe.Language
+import Cfe.Language.Base
+import Cfe.Language.Properties
+import Cfe.List.Compare
+import Cfe.Type
+import Cfe.Type.Base
+import Cfe.Type.Properties
+import Cfe.Vec.Relation.Binary.Pointwise.Inductive
diff --git a/cfe-proof.agda-lib b/cfe-proof.agda-lib
new file mode 100644
index 0000000..488beba
--- /dev/null
+++ b/cfe-proof.agda-lib
@@ -0,0 +1,4 @@
+name: cfe-proof
+depend: standard-library
+include: src
+flags: --safe --without-K