Make the usage of field keyword consistent

src/Ledger/Certs.lagda

@@ -38,11 +38,7 @@ instance
 \begin{NoConway}
 \begin{code}
 record PoolParams : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     rewardAddr : Credential
 \end{code}
 \end{NoConway}
@@ -92,25 +88,17 @@ cwitness (reg c (suc _))     = just c
 \begin{AgdaMultiCode}
 \begin{code}
 record CertEnv : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_,_,_⟧ᶜ
   field
-\end{code}
-\begin{code}
     epoch     : Epoch
     pp        : PParams
     votes     : List GovVote
     wdrls     : RwdAddr ⇀ Coin
     coldCreds : ℙ Credential
 
 record DState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ᵈ
   field
-\end{code}
-\begin{code}
     voteDelegs   : Credential ⇀ VDeleg
     stakeDelegs  : Credential ⇀ KeyHash
     rewards      : Credential ⇀ Coin
@@ -119,46 +107,30 @@ record DState : Type where
 \begin{code}
 
 record PState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_⟧ᵖ
   field
-\end{code}
-\begin{code}
     pools     : KeyHash ⇀ PoolParams
     retiring  : KeyHash ⇀ Epoch
 \end{code}
 \end{NoConway}
 \begin{code}
 
 record GState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_⟧ᵛ
   field
-\end{code}
-\begin{code}
     dreps      : Credential ⇀ Epoch
     ccHotKeys  : Credential ⇀ Maybe Credential
 
 record CertState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ᶜˢ
   field
-\end{code}
-\begin{code}
     dState : DState
     pState : PState
     gState : GState
 
 record DelegEnv : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ᵈᵉ
   field
-\end{code}
-\begin{code}
     pparams       : PParams
     pools         : KeyHash ⇀ PoolParams
     delegatees    : ℙ Credential

src/Ledger/Chain.lagda

@@ -26,19 +26,11 @@ open import Ledger.Certs govStructure
 \begin{AgdaMultiCode}
 \begin{code}
 record ChainState : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     newEpochState  : NewEpochState
 
 record Block : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     ts    : List Tx
     slot  : Slot
 \end{code}

src/Ledger/Crypto.lagda

@@ -19,34 +19,40 @@ record HashableSet : Type₁ where
   field T : Type; ⦃ T-isHashable ⦄ : isHashableSet T
   open isHashableSet T-isHashable public
 
-record PKKScheme : Type₁ where
-  field
 \end{code}
 We rely on a public key signing scheme for verification of spending.
 \begin{figure*}[h]
+\begin{AgdaMultiCode}
+\begin{code}[hide]
+record PKKScheme : Type₁ where
+  field
+\end{code}
 \emph{Types \& functions}
 \begin{code}
-        SKey VKey Sig Ser  : Type
-        isKeyPair          : SKey → VKey → Type
-        isSigned           : VKey → Ser → Sig → Type
-        sign               : SKey → Ser → Sig
+    SKey VKey Sig Ser  : Type
+    isKeyPair          : SKey → VKey → Type
+    isSigned           : VKey → Ser → Sig → Type
+    sign               : SKey → Ser → Sig
 
   KeyPair = Σ[ sk ∈ SKey ] Σ[ vk ∈ VKey ] isKeyPair sk vk
+
 \end{code}
-\emph{Property of signatures}
 \begin{code}[hide]
-  field ⦃ Dec-isSigned ⦄ : isSigned ⁇³
-        isSigned-correct :
+  field
+    ⦃ Dec-isSigned ⦄ : isSigned ⁇³
 \end{code}
+\emph{Property of signatures}
 \begin{code}
-          ((sk , vk , _) : KeyPair) (d : Ser) (σ : Sig) → sign sk d ≡ σ → isSigned vk d σ
+    isSigned-correct  : ((sk , vk , _) : KeyPair) (d : Ser) (σ : Sig)
+                      → sign sk d ≡ σ → isSigned vk d σ
 \end{code}
+\end{AgdaMultiCode}
 \caption{Definitions for the public key signature scheme}
 \label{fig:defs:crypto}
 \end{figure*}
 \begin{code}[hide]
-        ⦃ DecEq-Sig  ⦄ : DecEq Sig
-        ⦃ DecEq-Ser  ⦄ : DecEq Ser
+    ⦃ DecEq-Sig  ⦄ : DecEq Sig
+    ⦃ DecEq-Ser  ⦄ : DecEq Ser
 
 record Crypto : Type₁ where
   field pkk : PKKScheme

src/Ledger/Enact.lagda

@@ -34,22 +34,14 @@ since they are \HashProtected.
 \begin{AgdaMultiCode}
 \begin{code}
 record EnactEnv : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ᵉ
   field
-\end{code}
-\begin{code}
     gid       : GovActionID
     treasury  : Coin
     epoch     : Epoch
 
 record EnactState : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     cc            : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ))
     constitution  : HashProtected (DocHash × Maybe ScriptHash)
     pv            : HashProtected ProtVer

src/Ledger/Epoch.lagda

@@ -64,12 +64,8 @@ record Snapshots : Set where
 \end{NoConway}
 \begin{code}
 record EpochState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_,_,_⟧ᵉ'
   field
-\end{code}
-\begin{code}
     acnt       : Acnt
     ss         : Snapshots
     ls         : LState
@@ -79,12 +75,8 @@ record EpochState : Type where
 \begin{NoConway}
 \begin{code}
 record NewEpochState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ⁿᵉ
   field
-\end{code}
-\begin{code}
     lastEpoch   : Epoch
     epochState  : EpochState
     ru          : Maybe RewardUpdate

src/Ledger/Gov.lagda

@@ -41,12 +41,8 @@ GovState : Type
 GovState = List (GovActionID × GovActionState)
 
 record GovEnv : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_,_,_,_⟧ᵍ
   field
-\end{code}
-\begin{code}
     txid        : TxId
     epoch       : Epoch
     pparams     : PParams

src/Ledger/GovernanceActions.lagda

@@ -48,11 +48,7 @@ data VDeleg : Type where
   noConfidenceRep  :                         VDeleg
 
 record Anchor : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     url   : String
     hash  : DocHash
 
@@ -184,22 +180,14 @@ data Vote : Type where
   yes no abstain  : Vote
 
 record GovVote : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     gid         : GovActionID
     voter       : Voter
     vote        : Vote
     anchor      : Maybe Anchor
 
 record GovProposal : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     action      : GovAction
     prevAction  : NeedsHash action
     policy      : Maybe ScriptHash
@@ -208,11 +196,7 @@ record GovProposal : Type where
     anchor      : Anchor
 
 record GovActionState : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     votes       : Voter ⇀ Vote
     returnAddr  : RwdAddr
     expiresIn   : Epoch

src/Ledger/Introduction.lagda

@@ -144,11 +144,7 @@ over the state transition relation.
 \begin{AgdaMultiCode}
 \begin{code}
 record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Type) : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     compute     : C → S → Sig → Maybe S
     ≡-just⇔STS  : compute Γ s b ≡ just s' ⇔ Γ ⊢ s ⇀⦇ b ,X⦈ s'
 

src/Ledger/Ledger.lagda

@@ -34,25 +34,17 @@ defined transition systems.
 \begin{AgdaMultiCode}
 \begin{code}
 record LEnv : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_,_,_⟧ˡᵉ
   field
-\end{code}
-\begin{code}
     slot        : Slot
     ppolicy     : Maybe ScriptHash
     pparams     : PParams
     enactState  : EnactState
     treasury    : Coin
 
 record LState : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_,_⟧ˡ
   field
-\end{code}
-\begin{code}
     utxoSt     : UTxOState
     govSt      : GovState
     certState  : CertState

src/Ledger/NewPP.lagda

@@ -20,11 +20,7 @@ record NewPParamEnv : Type where
 \begin{code}
 record NewPParamState : Type where
   constructor ⟦_,_⟧ⁿᵖ
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     pparams  : PParams
     ppup     : PPUpdateState
 

src/Ledger/PPUp.lagda

@@ -24,20 +24,12 @@ private variable m n : ℕ
 GenesisDelegation = KeyHash ⇀ (KeyHash × KeyHash)
 
 record PPUpdateState : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     pup   : ProposedPPUpdates
     fpup  : ProposedPPUpdates
 
 record PPUpdateEnv : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     slot       : Slot
     pparams    : PParams
     genDelegs  : GenesisDelegation

src/Ledger/PParams.lagda

@@ -39,12 +39,8 @@ remain in treasury and reserves.
 \begin{AgdaMultiCode}
 \begin{code}
 record Acnt : Type where
-\end{code}
-\begin{code}[hide]
   constructor ⟦_,_⟧ᵃ
   field
-\end{code}
-\begin{code}
     treasury reserves : Coin
 
 ProtVer : Type
@@ -75,24 +71,14 @@ data PParamGroup : Type where
   SecurityGroup    : PParamGroup
 
 record DrepThresholds : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ
 
 record PoolThresholds : Type where
-\end{code}
-\begin{code}[hide]
   field
-\end{code}
-\begin{code}
     Q1 Q2a Q2b Q4 Q5e : ℚ
 
 record PParams : Type where
-\end{code}
-\begin{code}[hide]
   field
 \end{code}
 \emph{Network group}