diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 11:41:51 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 11:59:21 +0100 |
| commit | 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c (patch) | |
| tree | d9422bd08ee318b3fad90d03210f6a02a4c30783 /Everything.agda | |
| parent | 23e8afe152a84551491594aea133488523525410 (diff) | |
Add more properties for ordered structures.
Diffstat (limited to 'Everything.agda')
| -rw-r--r-- | Everything.agda | 21 |
1 files changed, 18 insertions, 3 deletions
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 |