IntersectMBO / IntersectMBO/formal-ledger-specifications
Groom open statements in specs
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
When working in #832, there was some discussion about hiding open statements [[link]](https://github.com/IntersectMBO/formal-ledger-specifications/pull/852#discussion_r2286764866).
The issue would be that readers are not expected to understand open statements, and therefore they need to be hidden. This in turn, induces other changes like using type classes or fully qualifying record fields to avoid introducing open statements to begin with.
I think explaining open statements, or a limited form of it, in some preliminary section doesn't look like a large burden, and it would simplify maintenance. I also find debatable that type classes (i.e. instance arguments) are going to be easier to understand.
Failing that, we should make a pass over the entire specs to hide open statements everywhere. A better alternative is to modify the html generation to hide open statements by default. If we ever want to show them in documentation, we could perhaps signal them with a special comment (e.g. `open LState -- htmlgenerator: expose`).
Contributor guide
Assessment
This issue has not been assessed yet.