blob: 5f0a1732f7a4586c55a8ca7338dd6f76957d9337 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
------------------------------------------------------------------------
-- Agda Helium
--
-- All library modules, along with short descriptions.
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
module Everything where
-- 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
import Helium.Semantics.Denotational
-- Base definitions for the denotational semantics.
import Helium.Semantics.Denotational.Core
|
