From 1f718c9dbe48934edf115aef285c5aeaa2dfb20d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Fri, 7 Jan 2022 13:36:42 +0000
Subject: Add some required algebraic types.

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

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index 5f0a173..1acafde 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -8,6 +8,21 @@
 
 module Everything where
 
+-- Definitions for more algebraic structures
+import Helium.Algebra.Bundles
+
+-- Relations between properties of functions when the underlying relation is a setoid
+import Helium.Algebra.Consequences.Setoid
+
+-- More core algebraic definitions
+import Helium.Algebra.Core
+
+-- More properties of functions
+import Helium.Algebra.Definitions
+
+-- Some more algebraic structures
+import Helium.Algebra.Structures
+
 -- Definition of types and operations used by the Armv8-M pseudocode.
 import Helium.Data.Pseudocode
 
-- 
cgit v1.2.3