IntersectMBO / IntersectMBO/formal-ledger-specifications
[Dijkstra] Move `Coin-TokenAlgebra` to a shared location
Open
discussion
easy
era: dijkstra
refactor
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
## Background
`src/Ledger/Dijkstra/Foreign/ExternalStructures.lagda.md` imports `Coin-TokenAlgebra` from `Ledger.Conway.Specification.TokenAlgebra.Coin`. The instance has no Conway-specific content, so the cross-era source dependency is incidental.
## Goal
Move `Coin-TokenAlgebra` (and the `Ledger.Conway.Specification.TokenAlgebra.Coin` module if appropriate) to a shared `Ledger.Core.*` location, or define a parallel `Ledger.Dijkstra.Specification.TokenAlgebra.Coin` that re-exports the same instance. Update `Ledger.Conway.Foreign.ExternalStructures` and `Ledger.Dijkstra.Foreign.ExternalStructures` to import from the new location.
Contributor guide
Assessment
This issue has not been assessed yet.