formal-ledger-specifications
formal-ledger-specifications copied to clipboard
Formatting STS rules
The formatting of let
seems weird to me and inconsistent across the document; I would suggest the following two versions to be applied uniformly and consistently:
- for very small binding, just keep it in the same line as the rule/constructor, e.g.
RULE: let x = 5 in ...
...
- for longer cases, always use the following format:
RULE:
let
BINDING #1
BINDING #2
...
BINDING #k
in
...
(if you cannot spare the two spaces caused by the suggested indentation, the problem lies elsewhere..)
While I'm at it, I saw some occurrences of the function arrow for rule hypotheses, which should be uniformly replaced with ∙
in my opinion and formatted the same way as LEDGER
currently is, i.e.
RULE : let ... in
∙ HYPOTHESIS #1
∙ HYPOTHESIS #2
∙ HYPOTHESIS #n
────────────────────────────────
CONCLUSION
(notice how the 'dots' lie outside and hypothesis, horizontal rule and conclusion are all lined up.
Originally posted by @omelkonian in https://github.com/IntersectMBO/formal-ledger-specifications/pull/336#discussion_r1430365405