PDF cleanup 282: hide data keyword

This addresses one item of issue #282.

src/Ledger/Deleg.lagda

@@ -15,7 +15,12 @@ open import Ledger.GovernanceActions gs
 record PoolParams : Set where
   field rewardAddr : Credential
 
-data DCert : Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  DCert : Set where
   delegate    : Credential → Maybe VDeleg → Maybe Credential → Coin → DCert
   dereg       : Credential → DCert
   regpool     : Credential → PoolParams → DCert
@@ -135,8 +140,11 @@ new certificates relating to DReps and the constitutional committee.
 \end{itemize}
 
 \begin{figure*}[h]
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Set where
+  _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Set where
   DELEG-delegate : let open PParams pp in
     ∙ (c ∉ dom rwds → d ≡ poolDeposit)
     ∙ (c ∈ dom rwds → d ≡ 0)
@@ -152,7 +160,12 @@ data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Set w
       ⟦ pp , pools ⟧ᵈᵉ ⊢  ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c ,DELEG⦈
                           ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
 
-data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set where
   POOL-regpool :
     ∙ c ∉ dom pools
       ────────────────────────────────
@@ -163,7 +176,12 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set whe
     ────────────────────────────────
     pp ⊢ ⟦ pools , retiring ⟧ᵖ ⇀⦇ retirepool c e ,POOL⦈ ⟦ pools , ❴ c , e ❵ ∪ˡ retiring ⟧ᵖ
 
-data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Set where
   GOVCERT-regdrep : let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
@@ -198,8 +216,11 @@ CERTBASE as the base case. CERTBASE does the following:
 \end{itemize}
 
 \begin{figure*}[h]
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Set where
+  _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Set where
   CERT-deleg :
     ∙ ⟦ pp , PState.pools stᵖ ⟧ᵈᵉ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
       ────────────────────────────────
@@ -215,7 +236,12 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → S
       ────────────────────────────────
       Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧ᶜˢ
 
-data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Set where
   CERT-base :
     let open PParams pp; open GState stᵍ; open DState stᵈ
         refresh         = mapPartial getDRepVote (fromList vs)

src/Ledger/Enact.lagda

@@ -81,9 +81,10 @@ required). The exceptions are \NewCommittee and \TreasuryWdrl:
 \end{itemize}
 
 \begin{figure*}[h]
-\begin{code}
+\begin{code}[hide]
 data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Set where
-
+\end{code}
+\begin{code}
   Enact-NoConf :
     ───────────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ NoConfidence ,ENACT⦈ record  s { cc = nothing , gid }

src/Ledger/GovernanceActions.lagda

@@ -27,14 +27,22 @@ maximum : ℙ ℚ → ℚ
 maximum x = foldl Data.Rational._⊔_ 0ℚ (proj₁ $ finiteness x)
 \end{code}
 \begin{figure*}[h]
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data GovRole : Set where
+  GovRole : Set where
   CC DRep SPO : GovRole
 
 Voter        = GovRole × Credential
 GovActionID  = TxId × ℕ
 
-data VDeleg : Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  VDeleg : Set where
   credVoter        : GovRole → Credential →  VDeleg
   abstainRep       :                         VDeleg
   noConfidenceRep  :                         VDeleg
@@ -43,7 +51,12 @@ record Anchor : Set where
   field  url   : String
          hash  : DocHash
 
-data GovAction : Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  GovAction : Set where
   NoConfidence     :                                             GovAction
   NewCommittee     : (Credential ⇀ Epoch) → ℙ Credential → ℚ  →  GovAction
   NewConstitution  : DocHash → Maybe ScriptHash               →  GovAction
@@ -136,7 +149,12 @@ HashProtected A = A × GovActionID
 
 \begin{figure*}[h]
 \begin{code}
-data Vote : Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  Vote : Set where
   yes no abstain  : Vote
 
 record GovVote : Set where

src/Ledger/PParams.lagda

@@ -41,7 +41,12 @@ record Acnt : Set where
 ProtVer : Set
 ProtVer = ℕ × ℕ
 
-data pvCanFollow : ProtVer → ProtVer → Set where
+\end{code}
+\begin{code}[hide]
+data
+\end{code}
+\begin{code}
+  pvCanFollow : ProtVer → ProtVer → Set where
   canFollowMajor : pvCanFollow (m , n) (m + 1 , 0)
   canFollowMinor : pvCanFollow (m , n) (m , n + 1)
 \end{code}
@@ -52,8 +57,11 @@ data pvCanFollow : ProtVer → ProtVer → Set where
 
 \begin{figure*}[h!]
 \begin{AgdaMultiCode}
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data PParamGroup : Set where
+  PParamGroup : Set where
   NetworkGroup EconomicGroup TechnicalGroup GovernanceGroup SecurityGroup : PParamGroup
 
 record DrepThresholds : Set where

src/Ledger/Script.lagda

@@ -56,10 +56,13 @@ record PlutusStructure : Set₁ where
         language : PlutusScript → Language
         toData : ∀ {A : Set} → A → Data
 \end{code}
-We define Timelock scripts here. They can verify the presence of keys and whether a transaction happens in a certain slot interval. These scripts are executed as part of the regular witnessing.
+We define \Timelock scripts here. They can verify the presence of keys and whether a transaction happens in a certain slot interval. These scripts are executed as part of the regular witnessing.
 \begin{figure*}[h]
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data Timelock : Set where
+  Timelock : Set where
   RequireAllOf       : List Timelock      → Timelock
   RequireAnyOf       : List Timelock      → Timelock
   RequireMOf         : ℕ → List Timelock  → Timelock
@@ -80,10 +83,11 @@ private variable
 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
+module _ (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) 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

src/Ledger/Utxo.lagda

@@ -114,9 +114,10 @@ module _ (let open Tx; open TxBody; open TxWitnesses) where opaque
 \end{code}
 \begin{code}[hide]
 module _ where
+  data
 \end{code}
 \begin{code}
-  data DepositPurpose : Set where
+    DepositPurpose : Set where
     CredentialDeposit  : Credential   → DepositPurpose
     PoolDeposit        : Credential   → DepositPurpose
     DRepDeposit        : Credential   → DepositPurpose
@@ -175,8 +176,11 @@ module _ (let open TxBody) where
 \begin{NoConway}
 \begin{figure*}
 \begin{AgdaMultiCode}
+\begin{code}[hide]
+data
+\end{code}
 \begin{code}
-data inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Set where
+  inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Set where
   both   : ∀ {l r}  → l ≤ slot × slot ≤ r  →  inInterval slot (just l   , just r)
   lower  : ∀ {l}    → l ≤ slot             →  inInterval slot (just l   , nothing)
   upper  : ∀ {r}    → slot ≤ r             →  inInterval slot (nothing  , just r)

src/latex/agda-latex-macros.sty

@@ -440,6 +440,7 @@
 \newcommand{\TechnicalGroup}{\AgdaInductiveConstructor{TechnicalGroup}\xspace}
 \newcommand{\THash}{\AgdaField{THash}\xspace}
 \newcommand{\threshold}{\AgdaFunction{threshold}\xspace}
+\newcommand{\Timelock}{\AgdaDatatype{Timelock}\xspace}
 \newcommand{\topNDRepDist}{\AgdaFunction{topNDRepDist}\xspace}
 \newcommand{\totalStake}{\AgdaFunction{totalStake}\xspace}
 \renewcommand{\trans}{\AgdaFunction{trans}\xspace}