You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 =5in ...
...
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.
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:(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 asLEDGER
currently is, i.e.(notice how the 'dots' lie outside and hypothesis, horizontal rule and conclusion are all lined up.
Originally posted by @omelkonian in #336 (comment)
The text was updated successfully, but these errors were encountered: