effect Carlos's change requests

Author: williamdemeo

src/Ledger/Dijkstra/Specification.lagda.md

@@ -2,9 +2,9 @@
 {-# OPTIONS --safe #-}
 module Ledger.Dijkstra.Specification where
 
-import Ledger.Dijkstra.Specification.Address
+import Ledger.Core.Specification.Address renaming (RwdAddr to RewardAddress)
 import Ledger.Dijkstra.Specification.Certs
-import Ledger.Dijkstra.Specification.Epoch
+import Ledger.Core.Specification.Epoch
 import Ledger.Dijkstra.Specification.Gov.Base
 import Ledger.Dijkstra.Specification.Gov.Actions
 import Ledger.Dijkstra.Specification.PParams

src/Ledger/Dijkstra/Specification/Address.lagda.md

@@ -4,11 +4,11 @@ source_path: src/Ledger/Dijkstra/Specification/PParams.lagda.md
 ---
 ```agda
 {-# OPTIONS --safe #-}
-open import Ledger.Dijkstra.Specification.Crypto
+open import Ledger.Core.Specification.Crypto
   using (CryptoStructure)
 open import Ledger.Dijkstra.Specification.Script
   using (ScriptStructure)
-open import Ledger.Dijkstra.Specification.Epoch
+open import Ledger.Core.Specification.Epoch
   using (EpochStructure)
 
 module Ledger.Dijkstra.Specification.PParams

src/Ledger/Dijkstra/Specification/Crypto.lagda.md

@@ -4,9 +4,9 @@ source_path: src/Ledger/Dijkstra/Specification/Script.lagda.md
 ---
 ```agda
 {-# OPTIONS --safe #-}
-open import Ledger.Dijkstra.Specification.Crypto
+open import Ledger.Core.Specification.Crypto
   using (CryptoStructure)
-open import Ledger.Dijkstra.Specification.Epoch
+open import Ledger.Core.Specification.Epoch
   using (EpochStructure)
 module Ledger.Dijkstra.Specification.Script
   (crypto : CryptoStructure)

src/Ledger/Dijkstra/Specification/Epoch.lagda.md

@@ -8,11 +8,11 @@ import Data.Maybe.Base as M
 
 open import Ledger.Prelude renaming (filterᵐ to filter)
 
-open import Ledger.Dijkstra.Specification.Crypto
-open import Ledger.Dijkstra.Specification.Epoch
+open import Ledger.Core.Specification.Crypto
+open import Ledger.Core.Specification.Epoch
 open import Ledger.Dijkstra.Specification.Gov.Base
 
-import Ledger.Dijkstra.Specification.Address
+import Ledger.Core.Specification.Address renaming (RwdAddr to RewardAddress)
 import Ledger.Dijkstra.Specification.Certs
 import Ledger.Dijkstra.Specification.Gov.Actions
 import Ledger.Dijkstra.Specification.PParams
@@ -98,7 +98,7 @@ record TransactionStructure : Type₁ where
   field crypto : _
   open CryptoStructure crypto public
   open Ledger.Dijkstra.Specification.TokenAlgebra.Base ScriptHash public
-  open Ledger.Dijkstra.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
+  open Ledger.Core.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
 
   field epochStructure : _
   open EpochStructure epochStructure public
@@ -141,8 +141,8 @@ record TransactionStructure : Type₁ where
   UTxO : Type
   UTxO = TxIn ⇀ TxOut
 
-  Withdrawals : Type
-  Withdrawals = RewardAddress ⇀ Coin
+  -- Withdrawals : Type
+  -- Withdrawals = RewardAddress ⇀ Coin
 
   -- Datums : Type
   -- Datums = DataHash ⇀ Datum

src/Ledger/Dijkstra/Specification/PParams.lagda.md

@@ -82,15 +82,15 @@ module Filter where
 
 -- TODO: Move to agda-sets
 -- https://github.com/input-output-hk/agda-sets/pull/13
-infixr 9 _∘ʳ_
-infix 10 _⁻¹ʳ
-opaque
-  _⁻¹ʳ : {A B : Type} → Rel A B → Rel B A
-  R ⁻¹ʳ = mapˢ swap R
-    where open import Data.Product using (swap)
-
-  _∘ʳ_ : {A B C : Type} ⦃ _ : DecEq B ⦄ → Rel A B → Rel B C → Rel A C
-  R ∘ʳ S =
-    concatMapˢ
-      (λ (a , b) → mapˢ ((a ,_) ∘ proj₂) $ filterˢ ((b ≡_) ∘ proj₁) S)
-      R
+-- infixr 9 _∘ʳ_
+-- infix 10 _⁻¹ʳ
+-- opaque
+--   _⁻¹ʳ : {A B : Type} → Rel A B → Rel B A
+--   R ⁻¹ʳ = mapˢ swap R
+--     where open import Data.Product using (swap)
+
+--   _∘ʳ_ : {A B C : Type} ⦃ _ : DecEq B ⦄ → Rel A B → Rel B C → Rel A C
+--   R ∘ʳ S =
+--     concatMapˢ
+--       (λ (a , b) → mapˢ ((a ,_) ∘ proj₂) $ filterˢ ((b ≡_) ∘ proj₁) S)
+--       R