blob: 039338b4470c006da10a0cfcb331c2d8ff8b1ff5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
------------------------------------------------------------------------
-- Agda Helium
--
-- All library modules, along with short descriptions.
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
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
-- Definitions of decidable algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Helium.Algebra.Decidable.Bundles
-- Construct decidable algebras of vectors in a pointwise manner
import Helium.Algebra.Decidable.Construct.Pointwise
-- Some decidable algebraic structures (not packed up with sets,
-- operations, etc.)
import Helium.Algebra.Decidable.Structures
-- More properties of functions
import Helium.Algebra.Definitions
-- Ordering properties of functions
import Helium.Algebra.Ordered.Definitions
-- Definitions of ordered algebraic structures like monoids and rings
-- (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
-- Algebraic properties of ordered commutative rings
import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
-- Algebraic properties of ordered division rings
import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing
-- Algebraic properties of ordered fields
import Helium.Algebra.Ordered.StrictTotal.Properties.Field
-- 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
-- Properties of almost groups
import Helium.Algebra.Properties.AlmostGroup
-- Some more algebraic structures
import Helium.Algebra.Structures
-- Definition of types and operations used by the Armv8-M pseudocode.
import Helium.Data.Pseudocode.Algebra
-- Algebraic properties of types used by the Armv8-M pseudocode.
import Helium.Data.Pseudocode.Algebra.Properties
-- Definition of the Armv8-M pseudocode.
import Helium.Data.Pseudocode.Core
-- Ways to modify pseudocode statements and expressions.
import Helium.Data.Pseudocode.Manipulate
-- Basic properties of the pseudocode data types
import Helium.Data.Pseudocode.Properties
-- Definition of instructions using the Armv8-M pseudocode.
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
-- 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
-- Definition of assertions used in correctness triples
import Helium.Semantics.Axiomatic.Assertion
-- Base definitions for the axiomatic semantics
import Helium.Semantics.Axiomatic.Core
-- Definition of terms for use in assertions
import Helium.Semantics.Axiomatic.Term
-- Definition of Hoare triples
import Helium.Semantics.Axiomatic.Triple
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core
|
