post-merge fixes and improvements

Author: williamdemeo

src/Ledger.lagda.md

@@ -12,5 +12,7 @@ import Ledger.Core
 import Ledger.Conway
 import Ledger.Dijkstra
 
+import Test.Examples
+
 import EssentialAgda
 ```

src/Ledger/Conway/Specification.lagda.md

@@ -124,13 +124,6 @@ import Ledger.Conway.Specification.Script
 import Ledger.Conway.Specification.Script.Validation
 ```
 
-## Tests and Examples
-
-```agda
-import Test.Examples
-import Test.StructuredContracts
-```
-
 ## Token Algebras
 
 ```agda

src/Test/Examples.lagda.md

@@ -7,7 +7,7 @@ The "Examples" module aims to add a couple of example smart contract
 validators written as part of the Cardano Formal Ledger Specification.
 These validator scripts are functions that examine a transaction and decide
 if the UTxO locked by their script can be spent as part of the current
-transaction. 
+transaction.
 
 <!--
 ```agda
@@ -30,7 +30,7 @@ of the UTxO rule, we also run the scripts locking any consumed outputs,
 which in our case are the validator scripts.
 
 The other examples are more in-depth and are separated across
-multiple modules. 
+multiple modules.
 
 ```agda
 import Test.Examples.MultiSig.Datum
@@ -69,8 +69,7 @@ Formal Ledger Rules.
 An "OffChain" folder, which defines the "endpoints" used to interact with
 our account. Essentially, this defines a way to easily create a transaction
 where we are attempting to execute one of the actions our validator
-might allow. This includes various aspects, such as making sure the transaction 
-
+might allow. This includes various aspects, such as making sure the transaction
 is signed by the right person, that the correct fees are paid, that payments
 are sent to the correct recipients, that the smart contract self-perpetuates, etc.
 
@@ -93,7 +92,7 @@ a payment. This trace succeeds and is tested with both the UTxO and UTxOw
 rules. We also have a failing trace, where after the first payment, we try
 to propose another payment of a larger amount than is contained in the wallet,
 which naturally fails.
- 
+
 ```agda
 import Test.Examples.AccountSim.Datum
 import Test.Examples.AccountSim.Validator

src/Test/Examples/AccountSim/Test/Trace.agda

@@ -47,9 +47,9 @@ data Tx' : Set where
     openn      : ℕ → Tx'
     close      : ℕ → Tx'
     withdraw   : ℕ → Value → Tx'
-    deposit    : ℕ -> Value -> Tx'
-    transfer   : ℕ -> ℕ -> Value -> Tx'
-    cleanup    : ℕ -> Tx'
+    deposit    : ℕ → Value → Tx'
+    transfer   : ℕ → ℕ → Value → Tx'
+    cleanup    : ℕ → Tx'
 
 
 makeTx : UTxOState → PlutusScript → Tx' → (id : ℕ) → Maybe Tx
@@ -82,7 +82,7 @@ evalTransanctionsW env (success s) (tx' ∷ txs') id =
   maybe
     (λ tx → evalTransanctions
               initEnv
-              (UTXO-stepW initEnv s tx)
+              (UTXO-step initEnv s tx)
               txs'
               (suc id))
     (failure "failed to generate tx")

src/Test/Examples/DEx/Test/Trace.agda

@@ -42,17 +42,17 @@ initState' : UTxO
 initState' = fromList' (createInitUtxoState 5 startValue)
 
 
-data Tx' : Set where   
+data Tx' : Set where
     start      : ℕ → Value → Q.ℚ → Tx'
     close      : ℕ → Tx'
     updatetx   : ℕ → Value → Q.ℚ → Tx'
     exchange   : ℕ → Value → Tx'
-    
+
 
 makeTx : UTxOState → PlutusScript → Tx' → (id : ℕ) → Maybe Tx
 makeTx s script (start w v r) id = just (startTx id w 999 v r script)
 makeTx s script (close w) id = makeCloseTx id s script w
-makeTx s script (updatetx w v r) id = makeUpdateTx id s script w v r 
+makeTx s script (updatetx w v r) id = makeUpdateTx id s script w v r
 makeTx s script (exchange w v) id = makeExchangeTx id s script w v
 
 evalTransanctions : UTxOEnv → ComputationResult String UTxOState → List Tx' → ℕ → ComputationResult String UTxOState
@@ -75,7 +75,7 @@ evalTransanctionsW env (success s) (tx' ∷ txs') id =
   maybe
     (λ tx → evalTransanctions
               initEnv
-              (UTXO-stepW initEnv s tx)
+              (UTXO-step initEnv s tx)
               txs'
               (suc id))
     (failure "failed to generate tx")
@@ -105,7 +105,7 @@ validTrace = start 5 (adaValueOf 80000000) rate
 
 validTrace2 : List Tx'
 validTrace2 = start 5 (adaValueOf 8000000000) rate
-              ∷ exchange 1 (adaValueOf 70000000) 
+              ∷ exchange 1 (adaValueOf 70000000)
               ∷ []
 
 
@@ -123,7 +123,7 @@ opaque
 
   evalValidTrace : ComputationResult String UTxOState
   evalValidTrace = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace 6
-  
+
   evalValidTrace2 : ComputationResult String UTxOState
   evalValidTrace2 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace2 6
 
@@ -137,4 +137,4 @@ opaque
   _ = refl
 
   _ : isSuccess evalFailingTrace ≡ false
-  _ = refl 
+  _ = refl

src/Test/Examples/MultiSig/Test/Trace.agda

@@ -78,7 +78,7 @@ evalTransanctionsW env (success s) (tx' ∷ txs') =
   maybe
     (λ tx → evalTransanctions
               initEnv
-              (UTXO-stepW initEnv s tx)
+              (UTXO-step initEnv s tx)
               txs')
     (failure "failed to generate tx")
     (makeTx s multiSigScript tx')

src/Test/Examples/MultiSigV2/Test/Trace.agda

@@ -85,7 +85,7 @@ evalTransanctionsW env (success s) (tx' ∷ txs') =
   maybe
     (λ tx → evalTransanctions
               initEnv
-              (UTXO-stepW initEnv s tx)
+              (UTXO-step initEnv s tx)
               txs')
     (failure "failed to generate tx")
     (makeTx s multiSigScript tx')