diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index d8c86bc..f57e5ba 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -31,7 +31,8 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
 module WithProg (prog : Program) where
     open Program prog
 
-    -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
+    -- The variable -> abstract value (e.g. sign) map is a finite value-map
+    -- with keys strings. Use a bundle to avoid explicitly specifying operators.
     module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
     open VariableValuesFiniteMap
         using ()
@@ -69,7 +70,7 @@ module WithProg (prog : Program) where
     fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
     ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
 
-    -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
+    -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
     module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
     open StateVariablesFiniteMap
         using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
@@ -170,7 +171,7 @@ module WithProg (prog : Program) where
                 ; f'-Monotonic to updateAll-Mono
                 )
 
-        -- Finally, the whole sign analysis consists of getting the 'join'
+        -- Finally, the whole analysis consists of getting the 'join'
         -- of all incoming states, then applying the per-state evaluation
         -- function. This is just a composition, and is trivially monotonic.
 
@@ -178,7 +179,9 @@ module WithProg (prog : Program) where
         analyze = updateAll ∘ joinAll
 
         analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
-        analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ = updateAll-Mono {joinAll sv₁} {joinAll sv₂} (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
+        analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ =
+            updateAll-Mono {joinAll sv₁} {joinAll sv₂}
+                           (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
 
         -- The fixed point of the 'analyze' function is our final goal.
         open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)