summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2021-12-27 17:21:32 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2021-12-27 17:44:55 +0000
commit87913c4014f01a23d608457e379b74aa1befd4ab (patch)
tree34d2405463757cf44089a795adb9a932e6707e50 /Everything.agda
parent0b581ec922b40284291d6814578bd2e68049c8b7 (diff)
Introduce Everything.agda to aid in overall compilation.
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda20
1 files changed, 20 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..5f0a173
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- All library modules, along with short descriptions.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Everything where
+
+-- Definition of types and operations used by the Armv8-M pseudocode.
+import Helium.Data.Pseudocode
+
+-- Definitions of a subset of Armv8-M instructions.
+import Helium.Instructions
+
+import Helium.Semantics.Denotational
+
+-- Base definitions for the denotational semantics.
+import Helium.Semantics.Denotational.Core