formal-ledger-specifications
formal-ledger-specifications copied to clipboard
Rearranging some of the duplicate code
- [ ] 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 some readability. - [ ] There are some files that will likely be completely identical between the two forever, for example
Address
and probablyTransaction
. Having duplication here comes at an actual cost, which is that we'd have to write conversion functions for everything to be able to prove equivalence. So I think for those files it'd be better to just import them. - [ ] The
Foreign
subtree probably makes more sense one level higher, i.e. inLedger.Conway
, especially given the previous point.
Originally posted by @WhatisRT in https://github.com/IntersectMBO/formal-ledger-specifications/pull/580#pullrequestreview-2328357124