4 files changed, 24 insertions, 2 deletions
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 9982501..7e6f6dc 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of types and operations used by the Armv8-M pseudocode.
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --without-K #-}
 
 module Helium.Data.Pseudocode where
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 5eba3f0..4bd02ac 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of a subset of Armv8-M instructions.
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --without-K #-}
 
 module Helium.Instructions where
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
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 54f0375..359fbd4 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -1,6 +1,10 @@
-{-# OPTIONS --safe --without-K #-}
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the denotational semantics.
+------------------------------------------------------------------------
 
-open import Helium.Data.Pseudocode
+{-# OPTIONS --safe --without-K #-}
 
 module Helium.Semantics.Denotational.Core
   {ℓ′}