fix alignment issues

Author: williamdemeo

src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

@@ -116,12 +116,12 @@ instance
     ; txscriptfee = λ tt y → 0
     ; serSize     = λ v → 0
     ; indexOfImp  = record
-      { indexOfDCert    = λ _ _ → nothing
+      { indexOfDCert          = λ _ _ → nothing
       ; indexOfRewardAddress  = λ _ _ → nothing
-      ; indexOfTxIn     = λ _ _ → nothing
-      ; indexOfPolicyId = λ _ _ → nothing
-      ; indexOfVote     = λ _ _ → nothing
-      ; indexOfProposal = λ _ _ → nothing
+      ; indexOfTxIn           = λ _ _ → nothing
+      ; indexOfPolicyId       = λ _ _ → nothing
+      ; indexOfVote           = λ _ _ → nothing
+      ; indexOfProposal       = λ _ _ → nothing
       }
     ; runPLCScript = λ _ _ _ _ → false
     ; scriptSize = λ where 

src/Ledger/Conway/Foreign/HSLedger/Gov/Actions.agda

@@ -18,7 +18,7 @@ data GovAction' : Type where
   NewConstitution     : DocHash → Maybe ScriptHash               →  GovAction'
   TriggerHardFork     : ProtVer                                  →  GovAction'
   ChangePParams       : PParamsUpdate                            →  GovAction'
-  TreasuryWithdrawal  : (RewardAddress ⇀ Treasury)                     →  GovAction'
+  TreasuryWithdrawal  : (RewardAddress ⇀ Treasury)               →  GovAction'
   Info                :                                             GovAction'
 
 instance

src/Ledger/Conway/Specification/Abstract.lagda.md

@@ -17,12 +17,12 @@ open import Ledger.Conway.Specification.Script.ScriptPurpose txs
 
 record indexOf : Type where
   field
-    indexOfDCert    : DCert → List DCert → Maybe Ix
-    indexOfRewardAddress  : RewardAddress → Withdrawals → Maybe Ix
-    indexOfTxIn     : TxIn → ℙ TxIn → Maybe Ix
-    indexOfPolicyId : ScriptHash → ℙ ScriptHash → Maybe Ix
-    indexOfVote     : GovVoter → List GovVoter → Maybe Ix
-    indexOfProposal : GovProposal → List GovProposal → Maybe Ix
+    indexOfDCert          : DCert          → List DCert        → Maybe Ix
+    indexOfRewardAddress  : RewardAddress  → Withdrawals       → Maybe Ix
+    indexOfTxIn           : TxIn           → ℙ TxIn            → Maybe Ix
+    indexOfPolicyId       : ScriptHash     → ℙ ScriptHash      → Maybe Ix
+    indexOfVote           : GovVoter       → List GovVoter     → Maybe Ix
+    indexOfProposal       : GovProposal    → List GovProposal  → Maybe Ix
 
 record AbstractFunctions : Type where
   field txscriptfee  : Prices → ExUnits → Coin

src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md

@@ -21,12 +21,12 @@ open import Ledger.Conway.Specification.Certs govStructure
 
 ```agda
 data ScriptPurpose : Type where
-  Cert     : DCert        → ScriptPurpose
-  Rwrd     : RewardAddress      → ScriptPurpose
-  Mint     : ScriptHash   → ScriptPurpose
-  Spend    : TxIn         → ScriptPurpose
-  Vote     : GovVoter     → ScriptPurpose
-  Propose  : GovProposal  → ScriptPurpose
+  Cert     : DCert          → ScriptPurpose
+  Rwrd     : RewardAddress  → ScriptPurpose
+  Mint     : ScriptHash     → ScriptPurpose
+  Spend    : TxIn           → ScriptPurpose
+  Vote     : GovVoter       → ScriptPurpose
+  Propose  : GovProposal    → ScriptPurpose
 
 record TxInfo : Type where
   field realizedInputs : UTxO

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

@@ -1,23 +1,24 @@
 ```agda
 {-# OPTIONS --safe #-}
 
-open import Ledger.Prelude
 open import Ledger.Dijkstra.Specification.Transaction
 
 module Ledger.Dijkstra.Specification.Abstract (txs : TransactionStructure) where
 
+open import Ledger.Prelude
 open TransactionStructure txs
 open import Ledger.Dijkstra.Specification.Certs govStructure
 
+
 record indexOf : Type where
   field
-    indexOfDCert    : DCert → List DCert → Maybe Ix
-    indexOfRewardAddress  : RewardAddress → Withdrawals → Maybe Ix
-    indexOfTxIn     : TxIn → ℙ TxIn → Maybe Ix
-    indexOfPolicyId : ScriptHash → ℙ ScriptHash → Maybe Ix
-    indexOfVote     : GovVoter → List GovVoter → Maybe Ix
-    indexOfProposal : GovProposal → List GovProposal → Maybe Ix
-    indexOfGuard    : TxId × ScriptHash → ℙ (TxId × ScriptHash) → Maybe Ix
+    indexOfDCert          : DCert              → List DCert             → Maybe Ix
+    indexOfRewardAddress  : RewardAddress      → Withdrawals            → Maybe Ix
+    indexOfTxIn           : TxIn               → ℙ TxIn                 → Maybe Ix
+    indexOfPolicyId       : ScriptHash         → ℙ ScriptHash           → Maybe Ix
+    indexOfVote           : GovVoter           → List GovVoter          → Maybe Ix
+    indexOfProposal       : GovProposal        → List GovProposal       → Maybe Ix
+    indexOfGuard          : TxId × ScriptHash  → ℙ (TxId × ScriptHash)  → Maybe Ix
 
 record AbstractFunctions : Type where
   field txScriptFee     : Prices → ExUnits → Fees

src/Test/AbstractImplementation.agda

@@ -24,12 +24,12 @@ SVAbstractFunctions = record
   ; txscriptfee = λ tt y → 0
   ; serSize     = λ v → 0 -- changed to 0
   ; indexOfImp  = record
-    { indexOfDCert    = λ _ _ → nothing
+    { indexOfDCert          = λ _ _ → nothing
     ; indexOfRewardAddress  = λ _ _ → nothing
-    ; indexOfTxIn     = indexOfTxInImp
-    ; indexOfPolicyId = λ _ _ → nothing
-    ; indexOfVote     = λ _ _ → nothing
-    ; indexOfProposal = λ _ _ → nothing
+    ; indexOfTxIn           = indexOfTxInImp
+    ; indexOfPolicyId       = λ _ _ → nothing
+    ; indexOfVote           = λ _ _ → nothing
+    ; indexOfProposal       = λ _ _ → nothing
     }
   ; runPLCScript = λ { x (sh , script) x₂ x₃ → script x₃ }
   ; scriptSize = λ _ → 0