From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 2 Apr 2022 11:41:51 +0100 Subject: Add more properties for ordered structures. --- Everything.agda | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'Everything.agda') diff --git a/Everything.agda b/Everything.agda index 8245737..3c60792 100644 --- a/Everything.agda +++ b/Everything.agda @@ -31,9 +31,6 @@ import Helium.Algebra.Decidable.Structures -- More properties of functions import Helium.Algebra.Definitions --- Redefine Ring monomorphisms to resolve problems with overloading. -import Helium.Algebra.Morphism.Structures - -- Ordering properties of functions import Helium.Algebra.Ordered.Definitions @@ -41,6 +38,12 @@ import Helium.Algebra.Ordered.Definitions -- (packed in records together with sets, operations, etc.) import Helium.Algebra.Ordered.StrictTotal.Bundles +-- Relations between algebraic properties of ordered structures +import Helium.Algebra.Ordered.StrictTotal.Consequences + +-- Morphisms for ordered algebraic structures. +import Helium.Algebra.Ordered.StrictTotal.Morphism.Structures + -- Algebraic properties of ordered abelian groups import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup @@ -50,9 +53,18 @@ import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing -- Algebraic properties of ordered groups import Helium.Algebra.Ordered.StrictTotal.Properties.Group +-- Algebraic properties of ordered magmas +import Helium.Algebra.Ordered.StrictTotal.Properties.Magma + +-- Algebraic properties of ordered monoids +import Helium.Algebra.Ordered.StrictTotal.Properties.Monoid + -- Algebraic properties of ordered rings import Helium.Algebra.Ordered.StrictTotal.Properties.Ring +-- Algebraic properties of ordered semigroups +import Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup + -- Some ordered algebraic structures (not packed up with sets, -- operations, etc.) import Helium.Algebra.Ordered.StrictTotal.Structures @@ -84,6 +96,9 @@ import Helium.Instructions.Core -- Implementation of Barrett reduction. import Helium.Instructions.Instances.Barrett +-- Relational properties of strict total orders +import Helium.Relation.Binary.Properties.StrictTotalOrder + -- Semantics for the Armv8-M pseudocode using Hoare triples. import Helium.Semantics.Axiomatic -- cgit v1.2.3