Other PDF cleanup items: Fig 5 (Token algebras) (#298)

* Other PDF cleanup items: Fig 5 (Token algebras)

Address an item in issue #289.

- [X] align the `field` keywords in the `TokenAlgebra` record type.
- [X] say what `PolicyID` is for.

* conform to pattern for displaying abstract types

Also change `\begin{figure*}[h]` to `\begin{figure*}[h!]` in `Address.lagda` so
that the figure appears on the same page as the section header, rather than a
mostly blank page under the header, preceding the figure.

src/Ledger/Address.lagda

@@ -68,13 +68,7 @@ Addr        = BaseAddr        ⊎ BootstrapAddr
 VKeyAddr    = VKeyBaseAddr    ⊎ VKeyBootstrapAddr
 ScriptAddr  = ScriptBaseAddr  ⊎ ScriptBootstrapAddr
 \end{code}
-\end{AgdaSuppressSpace}
-\end{AgdaAlign}
-\caption{Definitions used in Addresses}
-\label{fig:defs:addresses}
-\end{figure*}
-\begin{figure*}[h!]
-\begin{AgdaAlign}
+\end{AgdaSuppressSpace} \\
 \emph{Helper functions}
 \AgdaTarget{payCred, isVKeyAddr}
 \begin{code}
@@ -88,8 +82,8 @@ isScriptAddr     = isScript ∘ payCred
 isScriptRwdAddr  = isScript ∘ RwdAddr.stake
 \end{code}
 \end{AgdaAlign}
-\caption{Definitions used in Addresses, continued}
-\label{fig:defs:addresses-cont}
+\caption{Definitions used in Addresses}
+\label{fig:defs:addresses}
 \end{figure*}
 \begin{code}[hide]
 payCred (inj₁ record {pay = pay}) = pay

src/Ledger/TokenAlgebra.lagda

@@ -1,11 +1,18 @@
 \section{Token algebras}
 \label{sec:token-algebra}
-
+\begin{figure*}[h]
+\begin{AgdaAlign}
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
-module Ledger.TokenAlgebra (PolicyId : Set) where
-
+module Ledger.TokenAlgebra (
+\end{code}
+\emph{Abstract types}
+\begin{code}
+  PolicyId
+\end{code}
+\begin{code}[hide]
+  : Set) where
 open import Ledger.Prelude
 
 open import Algebra              using (CommutativeMonoid ; Monoid)
@@ -14,14 +21,16 @@ open import Data.Nat.Properties  using (+-0-monoid)
 open import Relation.Binary      using (Rel)
 open import Relation.Unary       using (Pred)
 \end{code}
-
-\begin{figure*}
+\emph{Derived types}
+\AgdaTarget{TokenAlgebra}
+\begin{AgdaSuppressSpace}
 \begin{code}
 record TokenAlgebra : Set₁ where
   field  Value-CommutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
 
   MemoryEstimate : Set
   MemoryEstimate = ℕ
+
 \end{code}
 \begin{code}[hide]
   open CommutativeMonoid Value-CommutativeMonoid public
@@ -41,6 +50,7 @@ record TokenAlgebra : Set₁ where
          property                  : coin ∘ inject ≗ id
          coinIsMonoidHomomorphism  : IsMonoidHomomorphism coin
 \end{code}
+\end{AgdaSuppressSpace}
 \begin{code}[hide]
          ⦃ DecEq-Value ⦄ : DecEq Value
          ⦃ Dec-≤ᵗ ⦄      : ∀ {v v′} → Dec (v ≤ᵗ v′)
@@ -49,9 +59,12 @@ record TokenAlgebra : Set₁ where
     addValue : HasAdd Value
     addValue = record { _+_ = _+ᵛ_ }
 \end{code}
+\emph{Helper functions}
+\AgdaTarget{sumᵛ}
 \begin{code}
   sumᵛ : List Value → Value
   sumᵛ = foldr _+ᵛ_ (inject 0)
 \end{code}
+\end{AgdaAlign}
 \caption{Token algebras, used for multi-assets}
 \end{figure*}