Andre Knispel
Andre Knispel
The question is what to do with the `\modulenote` macro. At the moment it produces a sentence that starts the section. This has the downside that it's a bit odd...
It was pointed out to me that the links in the introduction next to the tree of STSs are somewhat confusing, specifically these ones: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Introduction.lagda#L176 Every item links to both...
This issue is for keeping track of some magic numbers and what to do with them. - In Conway, a bunch of those go into `scriptsTotalSize`, since this was a...
We should first try to assess the necessity for this. So the questions to ask are: - where do we actually show dependent function and product types in the PDF,...
After some internal discussions, it seems we need to settle the question of how to present our STS relations. This is a follow-up to this comment: https://github.com/IntersectMBO/formal-ledger-specifications/issues/663#issuecomment-2633791011 The two main...
I'm collecting a bunch of feedback I've gotten yesterday [here](https://discord.com/channels/981862537513545788/1334557903369142333) in this issue. I'd like to address as much of this as we can so that hopefully the spec becomes...
We've had a small [discussion](https://github.com/IntersectMBO/formal-ledger-specifications/pull/661#discussion_r1937095942) that it might make more sense to just forbid zeros entirely in `TreasuryWdrl`, rather than to just force a single non-zero entry. We can't change...
That file has lots of lemmas that should live in https://github.com/input-output-hk/agda-sets.
See https://github.com/IntersectMBO/formal-ledger-specifications/issues/619#issuecomment-2520249922
@bwbush looked into the reserves recently, and discovered that `createRUpd` can in fact create a positive value for the reserves. The easiest way to see this is to assume that...