formal-ledger-specifications icon indicating copy to clipboard operation
formal-ledger-specifications copied to clipboard

Formatting STS rules

Open WhatisRT opened this issue 1 year ago • 0 comments

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:

  1. for very small binding, just keep it in the same line as the rule/constructor, e.g.
RULE: let x = 5 in ...
  ...
  1. 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

WhatisRT avatar Dec 19 '23 14:12 WhatisRT