summaryrefslogtreecommitdiff
path: root/src/Helium/Semantics/Denotational.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Semantics/Denotational.agda')
-rw-r--r--src/Helium/Semantics/Denotational.agda6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index fc93a26..c2a3f4f 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Denotational semantics of Armv8-M instructions.
+------------------------------------------------------------------------
+
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode