Readability of the figures

[WhatisRT]

Many figures in the Conway spec still have some typesetting problems. Here are some typical ones, all of them appear multiple times:

• [x] Too much whitespace when using vertical vectors (e.g. Fig. 22). Solve using AgdaSuppressSpace environments?
• [x] Some spacing issues with vertical vectors, e.g. Fig 24 at the bottom constMap wdrlCreds 0 ....
• [x] We shouldn't use qualified names, e.g. GovVote.voter and some others in Fig 14.
• [ ] It might make sense to replace some record construction with vertical vectors, e.g. in Fig 37.
• [x] Fitting figures on the page.
  • [x] Lines 107--113 of Gov.lagda: These lines do not fit in the figure box.
  • [x] Lines 309--351 of Certs.lagda: Figure 23 "CERTS rules" is too large to fit on the page without overlapping with the page number. We should either split up the figure, reduce white space in the figure, or suppress the page number on that page.
  • [x] Lines 106--154 of Enact.lagda: Figure 29 "ENACT transition system" is too big to fit on a page because of the new vertical vectors; we should split this up or find a way to compress white space or simply don't use vertical vectors here.
  • [X] ~Line 105 of Chain.lagda: "Fig 40: CHAIN transition system" has a line that's too long to fit in figure box.~ (in context of CHAIN sts; now context is just underscore)
  • [X] ~Lines 188--266 of Utxo.lagda: "Figure 12: Functions used in UTxO rules" shouldn't need its own page; the page before it is nearly blank; it would be much nicer if we could fit the figure on the previous page.~ (N/A: no longer true)
  • [X] Line 246 of Utxo.lagda: "Figure 12: Functions use in UTxO rules" with the new, larger harpoon arrow, this line no longer fits in the figure box.
  • [ ] "Figure 38: EPOCH transition system" doesn't fit on page; adding horizontal vector support to agda2vec script and making the first two vertical vectors in the figure horizontal should help.
• [x] Lines 155--171 of Utxo.lagda: "Figure 11: UTxO transition-system types" should have a blank line between Deposits = DepositPurpose ⇀ Coin and \emph{UTxO states}.
• [x] "Figure 15: Types and functions used in the GOV transition system": there should be a blank line before "Transition relation types" and before "Functions used in the GOV rules."
• [X] "Figure 16: Enactability predicate" uses qualified name GovActionState.action (could change this to action; probably just hiding open GovActionState in a hidden where block will type-check).
• [X] "Figure 16: Enactability predicate": fix alignment of cases in proof enactable and hasParentE.
• [X] "Figure 23: CERTS rules" uses qualified names RwdAddr.stake (could change to stake by adding open RwdAddr).
• [X] "Figure 28: ENACT transition system" uses qualified names .EnactState.cc and .PParams.ccMaxTermLength.
• [X] "Figure 37: Functions for computing stake distributions" uses qualified names RwdAddr.stake, GovActionState.returnAddr, .StakeDistrs.stakeDistr. (We probably can't unqualify the latter since there's also a function called stakeDistr in scope.)
• [ ] "Figure 41: CHAIN transition system": entailment after vertical vector should be inlined.

[williamdemeo]

Another one is the fact that some lines extend outside the figure box. I'll add that to the list.

Edit: added multiple sub-items under the item "Fitting figures on the page."