blob: 80dd812cfaaf4b9109c9bf01990ab44d80b89b17 (
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
|
------------------------------------------------------------------------
-- 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
-- Construct algebras of vectors in a pointwise manner
import Helium.Algebra.Construct.Pointwise
-- 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
-- Definitions of a subset of Armv8-M instructions.
import Helium.Instructions
-- Denotational semantics of Armv8-M instructions.
import Helium.Semantics.Denotational
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core
|
