IntersectMBO / IntersectMBO/formal-ledger-specifications

Other PDF cleanup items

Open
#289 2 comments 0 reactions 0 assignees View on GitHub
documentation latex
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.