IntersectMBO / IntersectMBO/ouroboros-consensus
Find way to call lemmas in consensus code
Open
- Dominant language
- Haskell
- Stars
- 67
- Forks
- 43
- Avg merge
- 5d 13h
- Merged PRs (30d)
- 43
Description
Lemmas `_lemma_protocoLedgerView_applyLedgerBlock` and `_lemma_ledgerViewForecastAt_applyChainTick` are no longer called (as of input-output-hk/ouroboros-network#2100), because they impose `Show` and `Eq` restrictions on the ledger view that are not satisfyable if they contain an `EpochInfo` (as in the hard fork combinator). It would be nice to find a way to reintroduce this, even if just in a limited fashion.
Contributor guide
Assessment
This issue has not been assessed yet.