formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
The formatting of `let` seems weird to me and inconsistent across the document; I would suggest the following two versions to be applied uniformly and consistently: 1. for very small...
I didn't have time for this in a long time, and there's a good chance there won't be time for it for a while, so I'm opening this issue to...
- [ ] Add support for inline datums - [x] Add withdrawals - [x] Add more rules to MAlonzo - [x] Add error messages when a computational rule fails
There is currently a repository that holds the executable spec which is manually updated. It would be nice to update it automatically, but it's easier to do it on a...
We currently use an ad-hoc shell command in `Makefile`: ```bash find $(HS_DIST)/MAlonzo -name "*.hs" -print\ | sed "s#^$(HS_DIST)/# #;s#\.hs##;s#/#.#g"\ >> $(HS_DIST)/$(CABAL_FILE) ``` ...but we should do it properly using [hpack](https://hackage.haskell.org/package/hpack)...
We now have `PreludeMeta` and `MetaPrelude`. There's probably some improvement to this structure that could be done at some point. _Originally posted by @WhatisRT in https://github.com/input-output-hk/formal-ledger-specifications/pull/301#discussion_r1391358656_
I still support the idea of having explicit constructs from Kleene algebra (*, +, ;, ε, maybe also ∪ for choice to have the full regex) to express this; e.g....
There are some files that we could generate as part of our build process instead of having them checked into the repo: - [ ] `agda.sty` - [ ] Everything...
This is a hint of the missing `Setoid/DecSetoid` interfaces, maybe worth a subsequent PR. _Originally posted by @omelkonian in https://github.com/input-output-hk/formal-ledger-specifications/pull/237#discussion_r1350493273_
One easy generalization of `Tactic.ByEq` that might be useful in a few places would be to take a tactic argument, and instead of unifying with `refl` instead try that tactic...