Skip to content

Commit a6dbc56

Browse files
committed
Add reference to definition of Deposits
1 parent d366a91 commit a6dbc56

File tree

3 files changed

+4
-1
lines changed

3 files changed

+4
-1
lines changed

src/Ledger/Certs.lagda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ instance
3131
((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
3232
\end{code}
3333
\caption{Deposit types}
34+
\label{fig:certs:deposit-types}
3435
\end{figure*}
3536

3637
\begin{figure*}[h!]

src/Ledger/Utxo.lagda

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,8 @@ is gone with the new design.
126126

127127
Similar to \ScriptPurpose, \DepositPurpose carries the information
128128
what the deposit is being made for. The deposits are stored in the
129-
\deposits field of \UTxOState. \updateDeposits is responsible for
129+
\deposits field of \UTxOState (the type \Deposits{} is defined in
130+
Figure~\ref{fig:certs:deposit-types}). \updateDeposits is responsible for
130131
updating this map, which is split into \updateCertDeposits and
131132
\updateProposalDeposits, responsible for certificates and proposals
132133
respectively. Both of these functions iterate over the relevant fields

src/latex/agda-latex-macros.sty

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,7 @@
236236
\newcommand{\DrepThresholds}{\AgdaRecord{DrepThresholds}\xspace}
237237
\newcommand{\drepThresholds}{\AgdaField{drepThresholds}\xspace}
238238
\newcommand{\DocHash}{\AgdaField{DocHash}\xspace}
239+
\newcommand{\Deposits}{\AgdaDatatype{Deposits}\xspace}
239240
\newcommand{\deposits}{\AgdaField{deposits}\xspace}
240241
\newcommand{\depositRefunds}{\AgdaFunction{depositRefunds}\xspace}
241242
\newcommand{\depositsChange}{\AgdaFunction{depositsChange}\xspace}

0 commit comments

Comments
 (0)