From 87913c4014f01a23d608457e379b74aa1befd4ab Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 27 Dec 2021 17:21:32 +0000
Subject: Introduce Everything.agda to aid in overall compilation.

---
 Everything.agda | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Everything.agda

(limited to 'Everything.agda')

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
-- 
cgit v1.2.3