Order PR fixes

- remove commented out code
- fix alignment broken by this PR
- add < for epochs specifically, so the PDF doesn't suffer

src/Interface/HasAdd/Instance.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --safe #-}
 module Interface.HasAdd.Instance where
 
-open import Interface.HasAdd  -- public
+open import Interface.HasAdd
 open import Data.Integer as ℤ using (ℤ)
 open import Data.Nat     as ℕ using (ℕ)
 

src/Ledger/Epoch.agda

@@ -131,14 +131,14 @@ record GlobalConstants : Set₁ where
 
   ℕEpochStructure : EpochStructure
   ℕEpochStructure = λ where
-    .Slotʳ → +-*-semiring
-    .Epoch → ℕ
-    .epoch slot → slot / SlotsPerEpochᶜ
-    .firstSlot e → e * SlotsPerEpochᶜ
-    ._≤ˢ_ → ℕ._≤_
-    .Slot-TO → ≤-isTotalOrder
+    .Slotʳ           → +-*-semiring
+    .Epoch           → ℕ
+    .epoch slot      → slot / SlotsPerEpochᶜ
+    .firstSlot e     → e * SlotsPerEpochᶜ
+    ._≤ˢ_            → ℕ._≤_
+    .Slot-TO         → ≤-isTotalOrder
     .StabilityWindow → StabilityWindowᶜ
-    .sucᵉ → suc
+    .sucᵉ            → suc
 
    where open EpochStructure
 

src/Ledger/Foreign/HSLedger.agda

@@ -90,7 +90,6 @@ HSEpochStructure  = EpochStructure  ∋ ℕEpochStructure HSGlobalConstants
 open import Ledger.PParams HSEpochStructure
 
 -- Dummy private key crypto scheme
--- open PKKScheme
 HSPKKScheme : PKKScheme
 HSPKKScheme = record
   { Implementation
@@ -100,23 +99,20 @@ HSPKKScheme = record
   ; isSigned-correct = λ where (sk , sk , refl) _ _ h → h
   }
 
--- open Crypto
 HSCrypto : Crypto
 HSCrypto = record
   { Implementation
   ; pkk = HSPKKScheme
   }
 
 -- No scripts for now
--- open P1ScriptStructure
 HSP1ScriptStructure : P1ScriptStructure ℕ ℕ ℕ
 HSP1ScriptStructure = record
   { Implementation
   ; validP1Script  = λ _ _ ()
   ; validP1Script? = λ _ _ ()
   }
 
--- open PlutusStructure
 HSP2ScriptStructure : PlutusStructure ℕ ℕ ℕ
 HSP2ScriptStructure = record
   { Implementation

src/Ledger/Gov.lagda

@@ -51,6 +51,10 @@ private variable
   addr : RwdAddr
   a : GovAction
   prev : NeedsHash a
+
+private -- FIXME: this should be part of a typeclass
+  _<_ : Epoch → Epoch → Set
+  a < b = a ≤ b × a ≢ b
 \end{code}
 \begin{code}
 -- could be implemented using a function of type:
@@ -85,7 +89,7 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovPropo
     actionWellFormed a ≡ true
     → d ≡ govActionDeposit
     →  (∀ {new rem q} → a ≡ NewCommittee new rem q
-       → ∀[ e ∈ range (new ˢ) ] epoch ≤ᵉ e × ¬ (epoch ≡ e) × dom (new ˢ) ∩ rem ≡ᵉ ∅)
+       → ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅)
     ────────────────────────────────
     let sig = inj₂ record { returnAddr = addr ; action = a ; anchor = x
                           ; deposit = d ; prevAction = prev }
@@ -135,7 +139,7 @@ instance
     case ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿
          ,′ isNewCommittee a of λ where
       (yesᵈ (wf , dep) , yesᵈ (new , rem , q , refl)) →
-        case ¿ ∀[ e ∈ range (new ˢ) ] epoch ≤ᵉ e × ¬ (epoch ≡ e) × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ of λ where
+        case ¿ ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ of λ where
           (yesᵈ newOk) → just (_ , GOV-Propose wf dep λ where refl → newOk)
           (noᵈ _)      → nothing
       (yesᵈ (wf , dep) , noᵈ notNewComm) → just (_ , GOV-Propose wf dep λ isNewComm → ⊥-elim (notNewComm (_ , _ , _ , isNewComm)))
@@ -149,7 +153,7 @@ instance
     with ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿ | isNewCommittee a
   ... | noᵈ ¬p | _ = ⊥-elim (¬p (wf , dep))
   ... | yesᵈ _ | noᵈ notNewComm = refl
-  ... | yesᵈ _ | yesᵈ (new , rem , q , refl) with ¿ ∀[ e ∈ range (new ˢ) ] epoch ≤ᵉ e × ¬ (epoch ≡ e) × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ | ""
+  ... | yesᵈ _ | yesᵈ (new , rem , q , refl) with ¿ ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ | ""
   ...    | yesᵈ newOk | _ = refl
   ...    | noᵈ notOk  | _ = ⊥-elim (notOk (newOk refl))
 

src/Ledger/GovernanceActions.lagda

@@ -349,7 +349,6 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
 \end{figure*}
 
 \begin{code}[hide]
--- open import Interface.Decidable.Instance
 open Computational' ⦃...⦄
 
 instance