From affce23167fcbd58265c4faef5dbbb92401398bd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 8 Jan 2022 17:38:01 +0000
Subject: Update Everything.

---
 Everything.agda | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index 1acafde..80dd812 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -14,6 +14,9 @@ import Helium.Algebra.Bundles
 -- Relations between properties of functions when the underlying relation is a setoid
 import Helium.Algebra.Consequences.Setoid
 
+-- Construct algebras of vectors in a pointwise manner
+import Helium.Algebra.Construct.Pointwise
+
 -- More core algebraic definitions
 import Helium.Algebra.Core
 
@@ -29,6 +32,7 @@ import Helium.Data.Pseudocode
 -- Definitions of a subset of Armv8-M instructions.
 import Helium.Instructions
 
+-- Denotational semantics of Armv8-M instructions.
 import Helium.Semantics.Denotational
 
 -- Base definitions for the denotational semantics.
-- 
cgit v1.2.3