IntersectMBO / IntersectMBO/formal-ledger-specifications
Other PDF cleanup items
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
This issue contains various items that don't really fit anywhere else. I've divided this into smaller and bigger tasks. None of this is really urgent ATM, so we can do these once we have some more time.
Bigger tasks:
- [x] Remove `_ᶠᵐ` notation from sums by introducing a typeclass
- [x] #652
- [x] Can we remove `+ᵉ` somehow? We could change `HasAdd` so that `+`
can take to different types, and then for a ring define some
instances where you can always add natural numbers/integers. But
maybe we can do something easier?
- [x] #656
Smaller tasks:
- [x] Fig. 5 (Token algebras, used for multi-assets):
- [x] missing type or explanation of `PolicyID`
- [x] the two `field` keywords are misaligned, so may be unclear that all fields belong to `TokenAlgebra` record type.
- [ ] We have some levels in the figure that we should get rid of
- [x] `MemoryEstimate` doesn't need to be defined inside a `TokenAlgebra`, so we should move it outside of it (otherwise people may think there's a reason why it's defined right there)
- [ ] Fig. 6 (Definitions used in Addresses):
- [ ] `isVKey` should be defined
- [ ] `isScript` should be defined
- [ ] why is `Γ ⊢` used instead of say, `_ ⊢` when environment is irrelevant?
- [ ] Fig. 22 (Definitions used in the UTxO transition system):
- [ ] different font for abstract types than Fig. 6
- [x] figure doesn't fit on the page
- [x] `mapPartial` needs to be defined
- [x] `isInj_1` needs to be defined
- [ ] Fig. 23 (Functions used in UTxO rules): define `mapKeys`
- [ ] Fig. 28 (Functions used for witnessing):
- [ ] Fig. 30 (UTXOW inference rules):
- [ ] `txidBytes` should be defined
- [ ] `hash` should be defined
- [x] Fig. 21 (Functions used in UTxO rules) is too big
- [x] Change notation for summation from `Σ` to `∑`
Contributor guide
Assessment
This issue has not been assessed yet.