summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda11
1 files changed, 4 insertions, 7 deletions
diff --git a/Everything.agda b/Everything.agda
index c88f419..f3f1bda 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -48,20 +48,17 @@ import Helium.Algebra.Ordered.StrictTotal.Structures
-- Some more algebraic structures
import Helium.Algebra.Structures
--- Definition of instructions using the Armv8-M pseudocode.
-import Helium.Data.Pseudocode
-
-- Definition of the Armv8-M pseudocode.
import Helium.Data.Pseudocode.Core
-- Definition of types and operations used by the Armv8-M pseudocode.
import Helium.Data.Pseudocode.Types
--- Definitions of a subset of Armv8-M instructions.
-import Helium.Instructions
+-- Definition of instructions using the Armv8-M pseudocode.
+import Helium.Instructions.Base
--- Denotational semantics of Armv8-M instructions.
-import Helium.Semantics.Denotational
+-- Definitions of the data for a subset of Armv8-M instructions.
+import Helium.Instructions.Core
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core