PDF cleanup 282: hide module syntax

This addresses one item of issue #282.
IntersectMBO · Feb 15, 2024 · bcc8a5c · bcc8a5c
1 parent 625e8c6
commit bcc8a5c
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 3 deletions.
diff --git a/src/Ledger/Script.lagda b/src/Ledger/Script.lagda
@@ -81,9 +81,19 @@ open import Data.List.Relation.Binary.Sublist.Ext
 open import Data.List.Relation.Binary.Sublist.Propositional as S
 import Data.Maybe.Relation.Unary.Any as M
 \end{code}
+\begin{code}[hide]
+module _
+\end{code}
+\begin{code}
+  (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot)
+\end{code}
+\begin{code}[hide]
+  where
+  data
+\end{code}
 \begin{code}
-module _ (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) where
-  data evalTimelock : Timelock → Set where
+
+    evalTimelock : Timelock → Set where
     evalAll  : All evalTimelock ss
              → evalTimelock (RequireAllOf ss)
     evalAny  : Any evalTimelock ss

diff --git a/src/Ledger/TokenAlgebra/ValueSet.lagda b/src/Ledger/TokenAlgebra/ValueSet.lagda
@@ -61,19 +61,27 @@ open CommutativeMonoid renaming (_∙_ to _⋆_) hiding (refl ; sym ; trans)
 
 AssetId  = PolicyId × AssetName
 Quantity = ℕ
-
+\end{code}
+\begin{code}[hide]
 module _
+\end{code}
+\begin{code}
+
   {X : ℙ AssetId}
   {⋁A : isMaximal X}
   ⦃ DecEq-PolicyId  : DecEq PolicyId ⦄
   ⦃ DecEq-AssetName : DecEq AssetName ⦄
   ⦃ DecEq-Tot : DecEq (AssetId ⇒ ℕ) ⦄
   (Dec-lookup≤ : ∀ {u v : AssetId ⇒ ℕ}
     → (∀ {a p q} → lookup u (a , p) ≤ lookup v (a , q)) ⁇)
+\end{code}
+\begin{code}[hide]
   where
 
   open ≡-Reasoning
   open FunTot X ⋁A
+\end{code}
+\begin{code}
 
   _⊕_ : Op₂ (AssetId ⇒ Quantity)
   u ⊕ v = Fun⇒TotalMap λ aa → (lookup u) aa + (lookup v) aa