PDF cleanup 282: hide use of open for records in pdf

src/Ledger/Chain.lagda

@@ -99,9 +99,13 @@ data
 \begin{figure*}[h]
 \begin{code}
   CHAIN :
+\end{code}
+\begin{code}[hide]
     let open ChainState s; open Block b; open NewEpochState newEpochState
         open EpochState epochState; open EnactState es
     in
+\end{code}
+\begin{code}
        record { stakeDistrs = calculateStakeDistrs ls }
          ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
     →  ⟦ slot , constitution .proj₁ .proj₂ , pparams .proj₁ , es ⟧ˡᵉ

src/Ledger/Epoch.lagda

@@ -72,14 +72,18 @@ its results, i.e:
 
 \begin{figure*}[h]
 \begin{code}
-  EPOCH : let
+  EPOCH :
+\end{code}
+\begin{code}[hide]
+    let
       open EpochState eps hiding (es)
       open RatifyState fut using (removed) renaming (es to esW)
       -- ^ this rolls over the future enact state into es
       open LState ls; open UTxOState utxoSt; open CertState certState
       open PState pState; open DState dState; open GState gState
       open Acnt acnt
-
+\end{code}
+\begin{code}
       trWithdrawals   = esW .EnactState.withdrawals
       totWithdrawals  = ∑[ x ← trWithdrawals ] x
 
@@ -108,7 +112,11 @@ its results, i.e:
 
       acnt' = record acnt
         { treasury = treasury + fees + unclaimed + donations ∸ totWithdrawals }
+\end{code}
+\begin{code}[hide]
     in
+\end{code}
+\begin{code}
     record { currentEpoch = e ; treasury = treasury ; GState gState ; NewEpochEnv Γ }
         ⊢ ⟦ es , ∅ , false ⟧ʳ ⇀⦇ govSt' ,RATIFY⦈ fut'
     ────────────────────────────────

src/Ledger/Gov.lagda

@@ -100,21 +100,31 @@ compatible version.
 data _⊢_⇀⦇_,GOV'⦈_ where
 \end{code}
 \begin{code}
-  GOV-Vote : ∀ {x ast} → let
+  GOV-Vote :
+\end{code}
+\begin{code}[hide]
+    ∀ {x ast} → let
       open GovEnv Γ
       sig = inj₁ record { gid = aid ; voter = voter ; vote = v ; anchor = x }
     in
+\end{code}
+\begin{code}
     ∙ (aid , ast) ∈ fromList s
     ∙ canVote pparams (action ast) (proj₁ voter)
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ sig ,GOV'⦈ addVote s aid voter v
 
-  GOV-Propose : ∀ {x} → let
+  GOV-Propose :
+\end{code}
+\begin{code}[hide]
+    ∀ {x} → let
       open GovEnv Γ; open PParams pparams hiding (a)
       prop = record { returnAddr = addr ; action = a ; anchor = x
                     ; policy = p ; deposit = d ; prevAction = prev }
       s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
     in
+\end{code}
+\begin{code}[hide]
     ∙ actionWellFormed a ≡ true
     ∙ d ≡ govActionDeposit
     ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy)

src/Ledger/Ledger.lagda

@@ -44,6 +44,8 @@ record LState : Set where
 
 txgov : TxBody → List (GovVote ⊎ GovProposal)
 txgov txb = map inj₁ txvote ++ map inj₂ txprop
+\end{code}
+\begin{code}[hide]
   where open TxBody txb
 \end{code}
 \caption{Types and functions for the LEDGER transition system}
@@ -77,7 +79,12 @@ data
 
 \begin{figure*}[h]
 \begin{code}
-  LEDGER : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
+  LEDGER :
+\end{code}
+\begin{code}[hide]
+    let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
+\end{code}
+\begin{code}
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     ∙  ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
     ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'

src/Ledger/NewPP.lagda

@@ -46,13 +46,23 @@ data _⊢_⇀⦇_,NEWPP⦈_ : NewPParamEnv → NewPParamState → Maybe PParamsU
 \end{code}
 \begin{figure*}[h]
 \begin{code}
-  NEWPP-Accept : ∀ {Γ} → let open NewPParamState s; newpp = applyUpdate pparams upd in
-    viablePParams newpp
-    ────────────────────────────────
-    Γ ⊢ s ⇀⦇ just upd ,NEWPP⦈ ⟦ newpp , updatePPUp newpp ppup ⟧ⁿᵖ
+  NEWPP-Accept : ∀ {Γ} →
+\end{code}
+\begin{code}[hide]
+    let open NewPParamState s
+\end{code}
+\begin{code}
+        newpp = applyUpdate pparams upd
+\end{code}
+\begin{code}[hide]
+    in
+\end{code}
+\begin{code}
+        viablePParams newpp
+        ────────────────────────────────
+        Γ ⊢ s ⇀⦇ just upd ,NEWPP⦈ ⟦ newpp , updatePPUp newpp ppup ⟧ⁿᵖ
 
-  NEWPP-Reject : ∀ {Γ} →
-    Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ s
+  NEWPP-Reject : ∀ {Γ} → Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ s
 \end{code}
 \caption{NEWPP transition system}
 \end{figure*}

src/Ledger/PPUp.lagda

@@ -68,7 +68,12 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
 \begin{code}
   PPUpdateEmpty : Γ ⊢ s ⇀⦇ nothing ,PPUP⦈ s
 
-  PPUpdateCurrent : let open PPUpdateEnv Γ in
+  PPUpdateCurrent :
+\end{code}
+\begin{code}[hide]
+   let open PPUpdateEnv Γ in
+\end{code}
+\begin{code}
     dom pup ⊆ dom genDelegs
     → All (isViableUpdate pparams) (range pup)
     → slot + (2 * StabilityWindow) < firstSlot (sucᵉ (epoch slot))

src/Ledger/Ratify.lagda

@@ -503,21 +503,36 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov
 \end{code}
 \begin{figure*}[h!]
 \begin{code}
-  RATIFY-Accept : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
+  RATIFY-Accept :
+\end{code}
+\begin{code}[hide]
+    let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
+\end{code}
+\begin{code}
        accepted Γ es st
     →  ¬ delayed action prevAction es d
     →  ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es'
        ────────────────────────────────
        Γ ⊢  ⟦ es   , removed          , d                      ⟧ʳ ⇀⦇ a ,RATIFY'⦈
             ⟦ es'  , ❴ a ❵ ∪ removed  , delayingAction action  ⟧ʳ
 
-  RATIFY-Reject : let open RatifyEnv Γ; st = a .proj₂ in
+  RATIFY-Reject :
+\end{code}
+\begin{code}[hide]
+    let open RatifyEnv Γ; st = a .proj₂ in
+\end{code}
+\begin{code}
        ¬ accepted Γ es st
     →  expired currentEpoch st
        ────────────────────────────────
        Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , ❴ a ❵ ∪ removed , d ⟧ʳ
 
-  RATIFY-Continue : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
+  RATIFY-Continue :
+\end{code}
+\begin{code}[hide]
+    let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
+\end{code}
+\begin{code}
        ¬ accepted Γ es st × ¬ expired currentEpoch st
     ⊎  accepted Γ es st
        × ( delayed action prevAction es d

src/Ledger/TokenAlgebra/ValueSet.lagda

@@ -56,12 +56,14 @@ record AdaIdType : Type where
 
 An inhabitant of `Value` is a map denoting a finite collection of quantities of assets.
 
-\begin{code}
+\begin{code}[hide]
 open CommutativeMonoid renaming (_∙_ to _⋆_) hiding (refl ; sym ; trans)
-
+\end{code}
+\begin{code}
 AssetId  = PolicyId × AssetName
 Quantity = ℕ
-
+\end{code}
+\begin{code}[hide]
 module _
   {X : ℙ AssetId}
   {⋁A : isMaximal X}
@@ -74,7 +76,8 @@ module _
 
   open ≡-Reasoning
   open FunTot X ⋁A
-
+\end{code}
+\begin{code}
   _⊕_ : Op₂ (AssetId ⇒ Quantity)
   u ⊕ v = Fun⇒TotalMap λ aa → (lookup u) aa + (lookup v) aa
 
@@ -130,34 +133,44 @@ module _
     lookup tm aa + lookup ι aa  ≡⟨ cong (lookup tm aa +_) lookupι≡0 ⟩
     lookup tm aa + 0            ≡⟨ +-identityʳ (lookup tm aa) ⟩
     lookup tm aa                ∎
-
+\end{code}
+\begin{code}[hide]
   open IsSemigroup
   open IsMagma
+\end{code}
+\begin{code}
   isSemigrp : IsSemigroup _≋_ _⊕_
   isSemigrp .isMagma .isEquivalence        = ≋-isEquivalence
   isSemigrp .isMagma .∙-cong {u}{v}{x}{y}  = ⊕-cong {u}{v}{x}{y}
   isSemigrp .assoc                         = ⊕-assoc
-
+\end{code}
+\begin{code}[hide]
   open IsMonoid
+\end{code}
+\begin{code}
   ≋-⊕-ι-isMonoid : IsMonoid _≋_ _⊕_ ι
   ≋-⊕-ι-isMonoid .isSemigroup  = isSemigrp
   ≋-⊕-ι-isMonoid .identity     = ι-identity
 \end{code}
 
 We are now in a position to define the commutative monoid.
 
-\begin{code}
+\begin{code}[hide]
   open IsCommutativeMonoid
+\end{code}
+\begin{code}
   Vcm : CommutativeMonoid 0ℓ 0ℓ
   Vcm .Carrier                        = AssetId ⇒ Quantity
   Vcm ._≈_                            = _≋_
   Vcm ._⋆_                            = _⊕_
   Vcm .ε                              = ι
   Vcm .isCommutativeMonoid .isMonoid  = ≋-⊕-ι-isMonoid
   Vcm .isCommutativeMonoid .comm      = ⊕-comm
-
+\end{code}
+\begin{code}[hide]
   instance _ = toCommMonoid' Vcm
-
+\end{code}
+\begin{code}
   Value-TokenAlgebra :
     (specialPolicy : PolicyId)
     (specialAsset : AssetName)
@@ -177,12 +190,13 @@ We are now in a position to define the commutative monoid.
     ; Dec-≤ᵗ = λ {x}{y} → Dec-lookup≤ {x}{y}
     }
     where
-
     specId : AssetId
     specId = (specialPolicy , specialAsset)
-
+\end{code}
+\begin{code}[hide]
     open Update
-
+\end{code}
+\begin{code}
     totalMap↠coin : AssetId ⇒ Quantity → Coin
     totalMap↠coin tm = lookup tm specId
 
@@ -197,14 +211,17 @@ We are now in a position to define the commutative monoid.
 
     compose-to-id : totalMap↠coin ∘ coin↪totalMap ≗ id
     compose-to-id _ = lookup-update-id ι
+\end{code}
+\begin{code}[hide]
       where open LookupUpdate {X = X} {specId} {⋁A}
 
     open CommutativeMonoid Vcm                    using () renaming (rawMonoid to Vcm-mon)
     open CommutativeMonoid +-0-commutativeMonoid  using () renaming (rawMonoid to ℕ-mon)
     open IsMonoidHomomorphism                     using (isMagmaHomomorphism ; ε-homo)
     open IsMagmaHomomorphism                      using (isRelHomomorphism ; homo)
     open IsRelHomomorphism                        using () renaming (cong to ⟦⟧-cong)
-
+\end{code}
+\begin{code}
     CoinMonHom : IsMonoidHomomorphism Vcm-mon ℕ-mon totalMap↠coin
     CoinMonHom .isMagmaHomomorphism .isRelHomomorphism .⟦⟧-cong  = λ x → x
     CoinMonHom .isMagmaHomomorphism .homo                        = λ x y → ⊕-lemma x y

src/Ledger/Utxo.lagda

@@ -217,7 +217,11 @@ feesOK pp tx utxo = minfee pp utxo tx ≤ᵇ txfee
                       ∧ not (≟-∅ᵇ collateral)
                       )
   where
+\end{code}
+\begin{code}[hide]
     open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp
+\end{code}
+\begin{code}
     collateralRange  = range    (utxo ∣ collateral)
     bal              = balance  (utxo ∣ collateral)
 \end{code}
@@ -367,10 +371,14 @@ data _⊢_⇀⦇_,UTXO⦈_ where
 \begin{figure*}[h]
 \begin{code}
   UTXO-inductive :
+\end{code}
+\begin{code}[hide]
     let open Tx tx renaming (body to txb); open TxBody txb
         open UTxOEnv Γ renaming (pparams to pp)
         open UTxOState s
     in
+\end{code}
+\begin{code}
     ∙ txins ≢ ∅                              ∙ txins ⊆ dom utxo
     ∙ inInterval slot txvldt                 ∙ feesOK pp tx utxo ≡ true
     ∙ consumed pp s txb ≡ produced pp s txb  ∙ coin mint ≡ 0

src/Ledger/Utxow.lagda

@@ -33,7 +33,11 @@ credsNeeded utxo txb
   ∪  mapPartial (λ p → case p .GovProposal.policy of λ where
     (just sh)  → just (Propose  p , inj₂ sh)
     nothing    → nothing) (fromList txprop)
+\end{code}
+\begin{code}[hide]
   where open TxBody txb
+\end{code}
+\begin{code}
 
 witsVKeyNeeded : UTxO → TxBody → ℙ KeyHash
 witsVKeyNeeded = getVKeys ∘₂ mapˢ proj₂ ∘₂ credsNeeded
@@ -68,10 +72,15 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
 \end{code}
 \begin{code}
   UTXOW-inductive :
-    let open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits
-        open UTxOState s
-        witsKeyHashes     = mapˢ hash (dom vkSigs)
-        witsScriptHashes  = mapˢ hash scripts
+    let
+\end{code}
+\begin{code}[hide]
+      open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits
+      open UTxOState s
+\end{code}
+\begin{code}
+      witsKeyHashes     = mapˢ hash (dom vkSigs)
+      witsScriptHashes  = mapˢ hash scripts
     in
     ∙  ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ
     ∙  ∀[ s ∈ scriptsP1 ] validP1Script witsKeyHashes txvldt s