Formatting STS rules

[WhatisRT]

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 ...
  ...

2. 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]

I like the above formatting, but we should agree on something as a team. Then it should be documented and applied everywhere to close this issue.

[williamdemeo]

I was under the impression we even wanted to hide the let and in keywords. However, I'm in favor of keeping those keywords, especially since interleaving {code} and {code}[hide] blocks messes up indentation in such a way that the only fix is by tedious trial-and-error (which can be time-consuming since re-compilation of the pdf is not instantaneous).

In my latest PR, I decide to hide the part of the let... in block that opened modules. Is that what we want to do in general (i.e., hide open directives appearing in let ... in blocks)?

[WhatisRT]

I'm not sure about hiding let and in. The old specs didn't have anything that corresponds to them and instead a line of the form n := t was used to signify a definition instead of a predicate. We could do the same but instead use n = t, because = can never be used in a term outside of a let binding, so it's syntactically unambiguous. However, hiding it makes the Agda itself more cluttered, so if we can get good-looking figures with it being visible I think that's a price worth paying.

The thing with open is a whole different story of a similar flavour. The additional downside is that we'd have to explain open if we show it somewhere. However, we shouldn't just have bound names come out of nowhere. So if we hide an open we need to make sure that there's an explanation of where the names come from somewhere. For example, we could say something like 'if there's a unique PParams value in scope, we may refer to the protocol parameters contained in that directly'. If we do that, we can just have a hidden open PParams pp wherever we like. I think we could safely generalize this to records whose definition we show in the spec which should cover most of the cases we use open in visible areas. One easy way to avoid an open is something like let ⟦ x , y , z ⟧ = v in ..., but that doesn't scale to PParams (and I don't think let record { myParam = myParam } = v in ... is a good substitute here, it's more notation to explain and it's quite heavy).

Overall, I think what we need to do is to experiment a little. Pick a few STSs and play around with some of these things until we have a set of guidelines that make everything look reasonable. I suggest picking at least a very large rule (such as EPOCH) and two smaller rules to fine tune this.

I also think that this should be done all the way at the end, when we're doing the final round of polishing on the spec. Otherwise some other thing may come along and screw up formatting without being noticed.