formal-ledger-specifications icon indicating copy to clipboard operation
formal-ledger-specifications copied to clipboard

Rearranging some of the duplicate code

Open WhatisRT opened this issue 5 months ago • 0 comments

  • [ ] 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 probably Transaction. 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. in Ledger.Conway, especially given the previous point.

Originally posted by @WhatisRT in https://github.com/IntersectMBO/formal-ledger-specifications/pull/580#pullrequestreview-2328357124

WhatisRT avatar Sep 26 '24 12:09 WhatisRT