PDF cleanup: remove all \small directives

Remove all `\small` latex directives and change global Agda code font size to "small."

(Some code blocks were enclosed inside `{\small ... }` which resulted in inconsistent code font size across the document.)

src/Ledger/GovernanceActions.lagda

@@ -31,7 +31,6 @@ maximum : ℙ ℚ → ℚ
 maximum x = foldl Data.Rational._⊔_ 0ℚ (proj₁ $ finiteness x)
 \end{code}
 \begin{figure*}[h]
-{\small
 \begin{code}
 GovActionID : Set
 GovActionID = TxId × ℕ
@@ -61,7 +60,6 @@ actionWellFormed : GovAction → Bool
 actionWellFormed (ChangePParams x)  = ppdWellFormed x
 actionWellFormed _                  = true
 \end{code}
-} %% end small
 \caption{Governance actions}
 \label{defs:governance}
 \end{figure*}
@@ -157,7 +155,6 @@ Every governance action must be ratified by at least two of these three bodies u
 The type of action and the state of the governance system determines which bodies must ratify it.
 Ratified actions are then \defn{enacted} on-chain, following a set of rules (see Section~\ref{sec:enactment} and Figure~\ref{fig:enactment-types}).
 \begin{figure*}[h]
-{\small
 \begin{code}
 NeedsHash : GovAction → Set
 NeedsHash NoConfidence           = GovActionID
@@ -171,7 +168,6 @@ NeedsHash Info                   = ⊤
 HashProtected : Set → Set
 HashProtected A = A × GovActionID
 \end{code}
-} %% end small
 \caption{NeedsHash and HashProtected types}
 \label{fig:needshash-and-hashprotected-types}
 \end{figure*}
@@ -190,7 +186,6 @@ attached to the action we want to ratify.
 See Section~\ref{sec:ratification} for more on the ratification process.
 
 \begin{figure*}[h]
-{\small
 \begin{code}
 data Vote : Set where
   yes no abstain  : Vote
@@ -209,7 +204,6 @@ record GovProposal : Set where
         deposit     : Coin
         anchor      : Anchor
 \end{code}
-} %% end small
 \caption{Governance action proposals and votes}
 \label{defs:governance-votes}
 \end{figure*}
@@ -257,7 +251,6 @@ A record of type \EnactState represents the state for enacting a governance acti
 The latter contains fields for the constitutional committee, constitution,
 protocol version, protocol parameters, withdrawals from treasury, and treasury balance.
 \begin{figure*}[h]
-{\small
 \begin{code}
 record EnactEnv : Set where
   constructor ⟦_,_,_⟧ᵉ
@@ -276,7 +269,6 @@ ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credenti
 ccCreds (just x  , _)  = dom (x .proj₁)
 ccCreds (nothing , _)  = ∅
 \end{code}
-} %% end small
 \caption{Enactment types}
 \label{fig:enactment-types}
 \end{figure*}
@@ -310,7 +302,6 @@ The relation \ENACTsyntax is the transition relation for enacting a governance a
 It represents how the \agdaboundEnactState changes when a specific governance action is enacted
 (see Figure~\ref{fig:enact-transition-system}).
 \begin{figure*}[h]
-{\small
 \begin{code}
 data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Set where
 
@@ -345,7 +336,6 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
   Enact-Info :
     ⟦ gid , t , e ⟧ᵉ ⊢  s ⇀⦇ Info  ,ENACT⦈ s
 \end{code}
-} %% end small
 \caption{ENACT transition system}
 \label{fig:enact-transition-system}
 \end{figure*}

src/Ledger/PParams.lagda

@@ -23,7 +23,6 @@ module Ledger.PParams
   where
 \end{code}
 \begin{figure*}[h!]
-{\small
 \begin{AgdaAlign}
 \begin{code}
 ProtVer : Set
@@ -99,7 +98,6 @@ paramsWellFormed pp = 0 ∉ fromList
   where open PParams pp
 \end{code}
 \end{AgdaAlign}
-} %% End: small
 \caption{Protocol parameter declarations}
 \label{fig:protocol-parameter-declarations}
 \end{figure*}

src/Ledger/Ratify.lagda

@@ -99,7 +99,6 @@ instance
   _ = +-0-monoid
 \end{code}
 \begin{figure*}[h!]
-{\small
 \begin{code}
 record StakeDistrs : Set where
   field stakeDistr  : VDeleg ⇀ Coin
@@ -144,7 +143,6 @@ isDRepProp = to-sp (λ x → isDRep x ≟ true)
 isSPOProp : specProperty λ x → isSPO x ≡ true
 isSPOProp = to-sp (λ x → isSPO x ≟ true)
 \end{code}
-} %% end small
 \caption{Types and functions for the RATIFY transition system}
 \label{fig:types-and-functions-for-the-ratify-transition-system}
 \end{figure*}
@@ -232,7 +230,6 @@ restrictedDists coins rank dists = dists
         restrict dist = topNDRepDist rank dist ∪ᵐˡ mostStakeDRepDist dist coins
 \end{code}
 \begin{figure*}[h!]
-{\small
 \begin{code}
 actualVotes : RatifyEnv → CCData → (GovRole × Credential) ⇀ Vote → GovAction → PParams
             → VDeleg ⇀ Vote
@@ -287,7 +284,6 @@ actualVotes Γ cc votes ga pparams
           (TriggerHF _)  → true
           _              → false
 \end{code}
-} %% end small
 \caption{%Ratify i:
 Types and proofs for the ratification of governance actions}
 \label{fig:defs:ratify-i}
@@ -323,7 +319,6 @@ The code in Figure~\ref{fig:defs:ratify-i} defines some of the types required fo
   it accomplishes this by aggregating the results of \actualCCVotes, \actualPDRepVotes, and \actualDRepVotes.
 \end{itemize}
 \begin{figure*}[h!]
-{\small
 \begin{code}
 votedHashes : Vote → (VDeleg ⇀ Vote) → GovRole → ℙ VDeleg
 votedHashes v votes r = votes ⁻¹ v
@@ -335,14 +330,12 @@ votedAbstainHashes participatingHashes : (VDeleg ⇀ Vote) → GovRole → ℙ V
 votedAbstainHashes = votedHashes Vote.abstain
 participatingHashes votes r = votedYesHashes votes r ∪ votedHashes Vote.no votes r
 \end{code}
-} %% end small
 \caption{Calculation of the votes as they will be counted}
 \label{fig:defs:ratify-ii}
 \end{figure*}
 
 The code in Figure~\ref{fig:defs:ratify-ii} defines \votedHashes, which returns the set of delegates who voted a certain way on the given governance role.
 \begin{figure*}[h!]
-{\small
 \begin{code}[hide]
 abstract
 \end{code}
@@ -381,7 +374,6 @@ abstract
   expired : Epoch → GovActionState → Set
   expired current record { expiresIn = expiresIn } = expiresIn < current
 \end{code}
-} %% end small
 \caption{%%Ratify iii:
 Calculation of stake distributions}
 \label{fig:defs:ratify-iii}
@@ -397,7 +389,6 @@ The code in Figure~\ref{fig:defs:ratify-iii} defines yet more types required for
   \item \expired checks whether a governance action is expired in a given epoch.
 \end{itemize}
 \begin{figure*}[h!]
-{\small
 \begin{code}[hide]
 open EnactState
 \end{code}
@@ -455,7 +446,6 @@ abstract
   expired? : ∀ e st → Dec (expired e st)
   expired? e st = ¿ expired e st ¿
 \end{code}
-} %% end small
 \caption{%Ratify iv:
 Determination of the status of ratification of the governance action}
 \label{fig:defs:ratify-iv}
@@ -479,7 +469,6 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov
 
 \end{code}
 \begin{figure*}[h!]
-{\small
 \begin{code}
   RATIFY-Accept : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
        accepted Γ es st
@@ -507,7 +496,6 @@ _⊢_⇀⦇_,RATIFY⦈_  : RatifyEnv → RatifyState → List (GovActionID × Go
                  → RatifyState → Set
 _⊢_⇀⦇_,RATIFY⦈_ = SS⇒BS _⊢_⇀⦇_,RATIFY'⦈_
 \end{code}
-} %% end small
 \caption{The RATIFY transition system}
 \label{fig:ratify-transition-system}
 \end{figure*}

src/latex/agda.sty

@@ -358,8 +358,9 @@
 % ----------------------------------------------------------------------
 % The code environment.
 
-\newcommand{\AgdaCodeStyle}{}
-% \newcommand{\AgdaCodeStyle}{\tiny}
+%\newcommand{\AgdaCodeStyle}{}
+\newcommand{\AgdaCodeStyle}{\small}
+%\newcommand{\AgdaCodeStyle}{\tiny}
 
 \ifdefined\mathindent
   {}