blob: 87109e295297f2b219c0177e9a14d1f2c634e817 (
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
128
129
130
|
------------------------------------------------------------------------
-- 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
-- A proof of correctness for Barrett reduction.
import Helium.Data.Pseudocode.Algebra.Barrett
-- 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
-- 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
-- Definition of terms for use in assertions
import Helium.Semantics.Axiomatic.Term
-- Definition of Hoare triples
import Helium.Semantics.Axiomatic.Triple
-- Base definitions for semantics
import Helium.Semantics.Core
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core
-- Ring solver tactic using integers as coefficients
import Helium.Tactic.CommutativeRing.NonReflective
|
