import TotalMapOn module in Ledger.Prelude

(so Alasdaire's script test doesn't choke on missing `TotalMapOn.agdai` file)
IntersectMBO · Jul 15, 2023 · 47d0bcf · 47d0bcf
1 parent d8f5ade
commit 47d0bcf
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Ledger/Prelude.agda b/src/Ledger/Prelude.agda
@@ -86,6 +86,7 @@ open import Axiom.Set.Map th public
   renaming (Map to _⇀_)
 
 open import Axiom.Set.TotalMap th public
+open import Axiom.Set.TotalMapOn th
 
 open L.Decˡ public
   hiding (_∈?_; ≟-∅)