fix type-checking fails

IntersectMBO · Mar 22, 2023 · fd1d88b · fd1d88b
1 parent 7f31134
commit fd1d88b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 6 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -11,7 +11,6 @@ We use Agda version 2.6.3 and a patched version of the Agda Standard Library; th
 To install Agda locally and use that install with emacs, you can do the following:
 
 -  Build `agda` and `agda-mode` binaries by invoking the following: `nix-build -A agda -o ~/IOHK/ledger-agda`
-   ```
 
    *Note*. You need not have built/installed Agda prior to invoking this `nix-build` command (though it's okay if you have).
 

diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda
@@ -88,14 +88,13 @@ HSScriptStructure : ScriptStructure ℕ ℕ ℕ
 HSScriptStructure = record { p1s = HSP1ScriptStructure ; ps = HSP2ScriptStructure }
 
 open import Ledger.Transaction
-open import Ledger.TokenAlgebra
+open import Ledger.TokenAlgebra ℕ
 open import Data.Nat.Properties using (+-0-commutativeMonoid; _≟_)
 open import Data.Nat
 
 coinTokenAlgebra : TokenAlgebra
 coinTokenAlgebra = record
-  { PolicyId                = ℕ
-  ; Value-CommutativeMonoid = +-0-commutativeMonoid
+  { Value-CommutativeMonoid = +-0-commutativeMonoid
   ; coin                    = id
   ; inject                  = id
   ; policies                = λ x → ∅

diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda
@@ -66,8 +66,9 @@ This function must produce a unique id for each unique transaction body.
 
 
   field ss : Ledger.Script.ScriptStructure KeyHash ScriptHash Slot
-        instance DecEq-ADHash : DecEq ADHash
-        tokenAlgebra                        : TokenAlgebra
+        -- instance DecEq-ADHash : DecEq ADHash
+        tokenAlgebra : TokenAlgebra
+
 
   open TokenAlgebra tokenAlgebra hiding (Coin) public