Other PDF cleanup items: Fig 5 (Token algebras) #298
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Address an item in issue #289. - [X] align the `field` keywords in the `TokenAlgebra` record type. - [X] say what `PolicyID` is for.
WhatisRT
requested changes
Nov 10, 2023
src/Ledger/TokenAlgebra.lagda
Outdated
| @@ -53,5 +54,6 @@ record TokenAlgebra : Set₁ where | |||
| sumᵛ : List Value → Value | |||
| sumᵛ = foldr _+ᵛ_ (inject 0) | |||
| \end{code} | |||
| \caption{Token algebras, used for multi-assets} | |||
| \end{AgdaAlign} | |||
| \caption{Token algebras, used for multi-assets; \AgdaBound{PolicyId} specifies a type (e.g., with natural numbers) used to represent policy identifiers.} | |||
There was a problem hiding this comment.
We already have a pattern for this, see the figure right below (Definitions used in Addresses). Maybe that pattern isn't that great (if you don't like it, make an issue to change it everywhere), but this should still follow it otherwise it's confusing (is PolicyID not an abstract type?).
There was a problem hiding this comment.
Okay, I'll check out the existing pattern and conform.
PolicyID : Type is a parameter passed into this (the TokenAlgebra) module (so, yeah, I suppose it would be considered an "abstract type").
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.
|
@WhatisRT I think this PR is good to go now. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Address items in issue #289.
fieldkeywords in theTokenAlgebrarecord type.PolicyIDis for.[h!]to figure environment so the figure does not appear above the section heading ("4 Token algebras").Checklist