formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
We have two models right now, one under `Ledger` and one under `Ledger.Conway.Conformance`. They differ by some logic being moved from `CERTS` into `UTXO` but are otherwise identical. This means...
- [ ] None of the `Ledger.Conway.Conformance` modules need to be literate Agda files, we probably won't compile those into a pdf. Removing all that stuff also should help restore...
# Description # Checklist - [ ] Commit sequence broadly makes sense and commits have useful messages - [ ] Code is formatted according to [CONTRIBUTING.md](https://github.com/input-output-hk/formal-ledger-specifications/blob/master/CONTRIBUTING.md) - [ ] Self-reviewed...
This issue is for discussing the high-level roadmap for this project. Note that we may drop things off of here if we decide against them in the future. # Features...
Once Agda 2.7 makes it into [nixpkgs master](https://raw.githubusercontent.com/NixOS/nixpkgs/master/pkgs/development/haskell-modules/hackage-packages.nix) we should update (see the bottom of `CONTRIBUTING.md` on how to update `agda-nixpkgs`). This will unblock merging #488.
When https://github.com/agda/agda-stdlib/pull/2479 is merged, which port stdlib additions from this repo, the task is to update the stdlib dependency and remove all these lemmas/definitions about lists: - `Data/List/Ext.agda` - `Data/List/Ext/Properties.agda`...
