cardano-ledger.pdf clean up

[williamdemeo]

• Add vertical space after Abstract types list, before Derived types in all figures where there's currently no space.
• Show data keyword consistently. (It appears in some figures e.g., Fig 8, 9, 12, but not others e.g., Fig 7, 20, 24).
• Show record keyword consistently. (It appears in most figures, but hidden in some, e.g., record PKKScheme in Fig 3, record TransactionStructure in Fig 17.)
• Add vertical space before UTxO states and UTxO transitions in Fig 20.
• Fig 21 doesn't fit on page; split it up into multiple figures.
• Consistently show data keyword, type signature, and definition for all transition rules so they are much easier to make sense of.
  • Show data and where keyword in Fig 1 (_⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type).
  • In Fig 31, _⊢_⇀⦇_,GOV'⦈_ is hidden, which makes the line, _⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_}, at bottom of figure incomprehensible.)
  • Same for Fig 52, _⊢_⇀⦇_,RATIFY⦈_ defined in terms of _⊢_⇀⦇_,RATIFY'⦈_ but the latter is hidden.
  • Combine type signature and definition of LEDGER rule (Figs 41, 42) into one figure.
  • Same comment for CHAIN rule (Figs 58, 59).
  • Move type signature of ENACT rule to the figure containing its definition.
  • Show data keyword and type signature for EPOCH rule (Fig 55).
• Indentation in definition of isUnregisteredDRep in Fig 40 is off; same for def of acceptConds in Fig 51.
• There seems to be a figure box missing around some code in Section 17 (Epoch Boundary).
• Add module names to all figure captions so it's easier to find the complete definitions in the repository when one wants more details/clarity.
• Add citations to first column of Table 1.
• Fig 29 does not fit on the page, split it up
• On Fig 36 the transition for DELEG-delegate is broken up into multiple lines, making it a bit confusing to read

[WhatisRT]

My opinion on some of these things:

• The record for PKKScheme should not be shown. It's not some data we pass around, it's just an abstraction we use that happens to be a record. That's why that name doesn't even show up. Same goes for TransactionStructure and all other bundles of abstract functions and types.
• The data and where keywords for step relations also shouldn't be shown. If they were shown, for the non-dependently typed reader this goes from 'here are some relations between the following things with a bunch of rules' to 'wtf are these datatypes???'. Same goes for evalTimelock - the only reason this is a type is because it being a function made inference difficult or something. The only place where the data keyword makes sense is PParamGroup, because that's something you actually use as data.

[williamdemeo]

We should make a concerted effort to respond to community feedback and it seems the community finds the documentation cryptic. In my view, the obvious solution is to hide less and explain more about how things are defined in Agda.