IntersectMBO / IntersectMBO/formal-ledger-specifications
Fix TODO in governance actions
Open
enhancement
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
This issue keeps track of a TODO introduced by #703. To solve it we require a (dependent) pattern-matching tactic which ATM does not exist --- see https://github.com/agda/agda-stdlib-meta/issues/27.
Contributor guide
Assessment
This issue has not been assessed yet.