formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
We want to use set comprehension to write sets and maps. There are some difficulties: - The syntax keyword isn't powerful enough, but we could for example have a notation...
We currently just put the literate (LaTeX) Agda in the HTML output, which produces a bunch of garbage. It would be nice to have good-looking HTML output as well, but...
It would be great to support pattern matching in the conclusion of a rule, to avoid having to write a bunch of `let`'s and explicit binders at the beginning of...
We need to deal with branching. We should be able to turn a proof that only at most one constructor applies into an instance of `Computational`. This means that we'd...
The current computation strategy is incompatible with nested rules. To fix this, instead of having clauses return a boolean, we can have them return a `Maybe X`, and do a...
# Description This addresses issue #512 # Checklist - [x] Commit sequence broadly makes sense and commits have useful messages - [x] Code is formatted according to [CONTRIBUTING.md](https://github.com/input-output-hk/formal-ledger-specifications/blob/master/CONTRIBUTING.md) - [x]...
Those governance actions that cannot cause a script to run on proposal should prevent that proposal from being supplied. There should be a check next to `∙ (∃[ u ]...
- [ ] `genErrors` always generates fully qualified names. The output would be a lot more readable if we postprocess the string to remove those qualifiers. - [ ] We...
`ReflexiveTransitiveClosure` does the base case last, but it should be done first.
We currently only remove those GAs that are directly removed by enactment. We also need to remove those that become unenactable because of the removals. This means that in https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Epoch.lagda#L229...