summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda9
1 files changed, 3 insertions, 6 deletions
diff --git a/Everything.agda b/Everything.agda
index 2f76af0..87109e2 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -96,9 +96,6 @@ import Helium.Data.Pseudocode.Core
-- Ways to modify pseudocode statements and expressions.
import Helium.Data.Pseudocode.Manipulate
--- Basic properties of the pseudocode data types
-import Helium.Data.Pseudocode.Properties
-
-- Definition of instructions using the Armv8-M pseudocode.
import Helium.Instructions.Base
@@ -117,15 +114,15 @@ import Helium.Semantics.Axiomatic
-- Definition of assertions used in correctness triples
import Helium.Semantics.Axiomatic.Assertion
--- Base definitions for the axiomatic semantics
-import Helium.Semantics.Axiomatic.Core
-
-- Definition of terms for use in assertions
import Helium.Semantics.Axiomatic.Term
-- Definition of Hoare triples
import Helium.Semantics.Axiomatic.Triple
+-- Base definitions for semantics
+import Helium.Semantics.Core
+
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core