improvements

Author: williamdemeo

src/Ledger/Crypto.lagda

@@ -23,7 +23,7 @@ record HashableSet : Type₁ where
 We rely on a public key signing scheme for verification of spending.
 \begin{figure*}[h]
 \begin{AgdaMultiCode}
-\begin{code}
+\begin{code}[hide]
 record PKKScheme : Type₁ where
   field
 \end{code}
@@ -35,6 +35,7 @@ record PKKScheme : Type₁ where
     sign               : SKey → Ser → Sig
 
   KeyPair = Σ[ sk ∈ SKey ] Σ[ vk ∈ VKey ] isKeyPair sk vk
+
 \end{code}
 \begin{code}[hide]
   field

src/Ledger/PParams.lagda

@@ -436,7 +436,7 @@ something) and if it preserves well-formedness.
 
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}
-\begin{code}
+\begin{code}[hide]
 record PParamsDiff : Type₁ where
   field
 \end{code}

src/Ledger/TokenAlgebra.lagda

@@ -10,6 +10,7 @@ module Ledger.TokenAlgebra (
 \emph{Abstract types}
 \begin{code}
   PolicyId
+
 \end{code}
 \begin{code}[hide]
   : Type) where
@@ -40,6 +41,8 @@ record TokenAlgebra : Type₁ where
 
   open MonoidMorphisms (rawMonoid) (Monoid.rawMonoid +-0-monoid) public
   field
+\end{code}
+\begin{code}
     coin                      : Value → Coin
     inject                    : Coin → Value
     policies                  : Value → ℙ PolicyId

src/Ledger/Transaction.lagda

@@ -61,8 +61,11 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 \begin{code}
 record TransactionStructure : Type₁ where
   field
-    -- Abstract types
+\end{code}
+\emph{Abstract types}
+\begin{code}
     Ix TxId AuxiliaryData : Type
+
 \end{code}
 \begin{code}[hide]
     ⦃ DecEq-Ix   ⦄ : DecEq Ix