Skip to content

Commit

Permalink
Fix indentation of record fields in PDF (#651)
Browse files Browse the repository at this point in the history
* This affects Figures 17 and 44
  • Loading branch information
carlostome authored Jan 24, 2025
1 parent c5656b0 commit e32b210
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 4 deletions.
4 changes: 2 additions & 2 deletions src/Ledger/Enact.lagda
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ Note that all other fields of \EnactState also contain a \GovActionID
since they are \HashProtected.

\begin{figure*}[h]
\begin{AgdaSuppressSpace}
\begin{AgdaMultiCode}
\begin{code}
record EnactEnv : Type where
\end{code}
Expand Down Expand Up @@ -90,7 +90,7 @@ data
\begin{code}
_⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type
\end{code}
\end{AgdaSuppressSpace}
\end{AgdaMultiCode}
\caption{Types and function used for the ENACT transition system}
\label{fig:enact-defs}
\end{figure*}
Expand Down
3 changes: 1 addition & 2 deletions src/Ledger/Transaction.lagda
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi

\begin{figure*}[h]
\emph{Abstract types}
\begin{AgdaMultiCode}
\begin{code}
Ix TxId AuxiliaryData : Type
\end{code}
Expand Down Expand Up @@ -110,7 +109,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi
open GovernanceActions hiding (Vote; yes; no; abstain) public

open import Ledger.Certs govStructure using (DCert)

\end{code}
\begin{NoConway}
\emph{Derived types}
Expand All @@ -126,6 +124,7 @@ Ingredients of the transaction body introduced in the Conway era are the followi
\end{code}
\end{NoConway}
\emph{Transaction types}
\begin{AgdaMultiCode}
\begin{code}
record TxBody : Type where
\end{code}
Expand Down

0 comments on commit e32b210

Please sign in to comment.