IntersectMBO / IntersectMBO/formal-ledger-specifications

Groom open statements in specs

Open
#864 1 comment 0 reactions 0 assignees View on GitHub
documentation enhancement
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.