Change parameter of Ratify

carlostome · carlostome · commit 2fe03050bc42 · 2026-01-08T14:27:20.000+01:00
diff --git a/src/Ledger/Conway/Conformance/Chain.agda b/src/Ledger/Conway/Conformance/Chain.agda
@@ -15,7 +15,7 @@ module Ledger.Conway.Conformance.Chain
 
 open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Conformance.Ledger txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Epoch txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
diff --git a/src/Ledger/Conway/Conformance/Epoch.agda b/src/Ledger/Conway/Conformance/Epoch.agda
@@ -22,7 +22,7 @@ open import Ledger.Conway.Conformance.Equivalence txs abs
 open import Ledger.Conway.Conformance.Equivalence.Convert
 open import Ledger.Conway.Conformance.Equivalence.Deposits txs abs
 open import Ledger.Conway.Conformance.Ledger txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
diff --git a/src/Ledger/Conway/Conformance/Epoch/Properties.agda b/src/Ledger/Conway/Conformance/Epoch/Properties.agda
@@ -13,7 +13,7 @@ module Ledger.Conway.Conformance.Epoch.Properties
 
 open import Ledger.Conway.Conformance.Epoch txs abs
 open import Ledger.Conway.Conformance.Ledger txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Ratify.Properties.Computational txs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
diff --git a/src/Ledger/Conway/Conformance/Ledger/Properties.agda b/src/Ledger/Conway/Conformance/Ledger/Properties.agda
@@ -18,7 +18,7 @@ open import Ledger.Conway.Conformance.Certs.Properties govStructure
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Gov.Properties.Computational txs
 open import Ledger.Conway.Conformance.Ledger txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Utxo.Properties txs abs
 open import Ledger.Conway.Conformance.Utxow txs abs
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda
@@ -13,9 +13,9 @@ open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
 import Data.Rational.Show as Rational
 
 import Foreign.Haskell.Pair as F
-open import Ledger.Conway.Specification.Ratify it
+open import Ledger.Conway.Specification.Ratify govStructure
   hiding (acceptedByCC; acceptedByDRep; acceptedBySPO)
-import Ledger.Conway.Specification.Ratify it as Ratify
+import Ledger.Conway.Specification.Ratify govStructure as Ratify
 open import Ledger.Conway.Specification.Ratify.Properties.Computational it
 
 instance
diff --git a/src/Ledger/Conway/Specification/Chain.lagda.md b/src/Ledger/Conway/Specification/Chain.lagda.md
@@ -24,7 +24,7 @@ open import Ledger.Conway.Specification.Epoch txs abs
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Ledger txs abs
 open import Ledger.Prelude; open Equivalence
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.RewardUpdate txs abs
 open import Ledger.Conway.Specification.Utxo txs abs
 
diff --git a/src/Ledger/Conway/Specification/Epoch.lagda.md b/src/Ledger/Conway/Specification/Epoch.lagda.md
@@ -43,7 +43,7 @@ open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Ledger txs abs
 open import Ledger.Conway.Specification.PoolReap txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Rewards txs abs
 open import Ledger.Conway.Specification.Utxo txs abs
 
diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.lagda.md
@@ -24,7 +24,7 @@ open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Specification.Ledger txs abs
 open import Ledger.Conway.Specification.PoolReap txs abs
 open import Ledger.Conway.Specification.PoolReap.Properties.Computational txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Ratify.Properties.Computational txs
 open import Ledger.Conway.Specification.Rewards txs abs
 open import Ledger.Conway.Specification.Rewards.Properties.Computational txs abs
diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md
@@ -24,7 +24,7 @@ open import Ledger.Prelude hiding (cong)
 import Ledger.Prelude as P
 import Relation.Binary.Core as B
 open import Relation.Binary.Definitions
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure
 open import Ledger.Conway.Specification.Ledger txs abs
diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md
@@ -36,7 +36,7 @@ open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Ledger txs abs
 open import Ledger.Conway.Specification.Ledger.Properties.Base txs abs
 open import Ledger.Conway.Specification.PoolReap txs abs
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Utxo txs abs
 
 open import Axiom.Set.Properties th
diff --git a/src/Ledger/Conway/Specification/Gov.lagda.md b/src/Ledger/Conway/Specification/Gov.lagda.md
@@ -27,7 +27,7 @@ open import Axiom.Set.Properties th using (∃-sublist-⇔)
 
 open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)
 open import Ledger.Conway.Specification.Enact govStructure
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 open import Ledger.Conway.Specification.Certs govStructure
 
 open import stdlib.Data.List.Subpermutations using (subpermutations; sublists)
diff --git a/src/Ledger/Conway/Specification/Gov/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Gov/Properties/Computational.lagda.md
@@ -20,7 +20,7 @@ open import Axiom.Set.Properties
 open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no)
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 
 import Data.List.Membership.Propositional as P
 open import Data.List.Membership.Propositional.Properties
diff --git a/src/Ledger/Conway/Specification/Ratify.lagda.md b/src/Ledger/Conway/Specification/Ratify.lagda.md
@@ -10,9 +10,9 @@ source_path: src/Ledger/Conway/Specification/Ratify.lagda.md
 
 {-# OPTIONS --safe #-}
 
-open import Ledger.Conway.Specification.Transaction hiding (Vote)
+open import Ledger.Conway.Specification.Gov.Base
 
-module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where
+module Ledger.Conway.Specification.Ratify (govStructure : GovStructure) where
 
 import Data.Integer as ℤ
 open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
@@ -22,7 +22,8 @@ open import Ledger.Prelude hiding (_∧_; _∨_; _⊔_) renaming (filterᵐ to f
 
 open import Ledger.Conway.Specification.Certs govStructure
 open import Ledger.Conway.Specification.Enact govStructure
-open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)
+open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no)
+open GovStructure govStructure
 ```
 -->
 
diff --git a/src/Ledger/Conway/Specification/Ratify/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Ratify/Properties/Computational.lagda.md
@@ -15,7 +15,7 @@ open import Ledger.Prelude
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure
-open import Ledger.Conway.Specification.Ratify txs
+open import Ledger.Conway.Specification.Ratify govStructure
 
 open Computational ⦃...⦄ hiding (computeProof; completeness)
 
