Remove Ledger.Set, inline the main def in Ledger.Prelude

Author: carlostome

src/Ledger/Prelude.agda

@@ -29,8 +29,8 @@ open import Ledger.Interface.HasCoin public
 open import MyDebugOptions public
 open import Tactic.Premises public
 
-open import Ledger.Set public
-    renaming (_⊆_ to _⊆ˢ_)
+open import abstract-set-theory.FiniteSetTheory public
+  renaming (_⊆_ to _⊆ˢ_)
 
 dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q
 dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p
@@ -50,3 +50,6 @@ instance
 
 ≡ᵉ-getCoin : ∀ {A} → ⦃ _ : DecEq A ⦄ → (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s'
 ≡ᵉ-getCoin {A} ⦃ decEqA ⦄ s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s'
+
+setToMap : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ℙ (A × B) → A ⇀ B
+setToMap = fromListᵐ ∘ setToList

src/Ledger/Set.agda

@@ -222,7 +222,7 @@ record TransactionStructure : Type₁ where
       just (lookupᵐ m sh)
     else
       nothing
-    where m = setToHashMap (txscripts tx utxo)
+    where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))
 \end{code}
 \end{AgdaMultiCode}
 \caption{Functions related to transactions}