summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda3
1 files changed, 3 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
index f3f1bda..aa36309 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -60,5 +60,8 @@ import Helium.Instructions.Base
-- Definitions of the data for a subset of Armv8-M instructions.
import Helium.Instructions.Core
+-- Implementation of Barrett reduction.
+import Helium.Instructions.Instances.Barrett
+
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core