652 remove superscripts from rec constr

[carlostome]

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[carlostome]

This is currently blocked by #653

[WhatisRT]

I really like this, but it's a shame that we're losing some of the patterns here. I think some of them should be resurrected. Here's the most obvious place where things got worse. Before:

After:

Obviously this has other issues as well, but in the before it's really easy to see what changed and maybe more crucially what didn't change (and that e.g. the reserves and treasury didn't get swapped), and in the after this is completely gone (and just adding the vertical vectors back in isn't going to fix it). There are a few other places such as UTXOW.

It's a shame that it's not quite as powerful as Lean's ⟨ ⟩ which also functions as a pattern on the LHS, but there probably isn't much we can do about that. I think in the above cases, it would be good to keep the patterns around just to render those more nicely.

Maybe it could be a future AIM project to get such record patterns that can be used for matching as well?

[carlostome]

The before/after differences are due to a bug in the agda2vec.py script (see #666) not of this PR really

[WhatisRT]

If #666 is fixed then it still doesn't resolve the problem. In the before picture, the LHS provides quite a lot of information visually, just by being able to line up matching entries on the RHS. This gets lost completely if the LHS is just applyRUpd ru epochState.

[williamdemeo]

Update re. eliminating constructors on LHS of applyRUpd def.

Here's what the output looks like now that the agda2vec script is working with @carlostome's new constructor type class.