Andre Knispel

The potential downsides here are: - this uses dependent types visibly in the documentation - we can't do `open PParams pp` anymore (thought I guess we could make a big...

In principle it shouldn't be too difficult to turn the formal specification into one that can operate on CBOR serialized data. We already have a translation for most datatypes that...

> You mean to say that you are volunteering for this task 😶 ? > I don't really have time to work on this myself (too busy with Leios), but...

> * Only operates on the outermost level, i.e. `LEDGER` rule that takes a ledger state and transition is a `Tx` > > * This is quite black-boxy, but maybe...

Overall, this sounds quite reasonable to me. Some points I'd like to add: 1. A ledger implementation that wants to participate in consensus will have to be able to validate...

I think we do have an explanation of `ReflexiveTransitiveClosure` somewhere in the introduction, but the `ᵇ'` part doesn't help of course. Some cleanup might be necessary here.

I think it's probably related to https://github.com/agda/agda/issues/7290 and the even further upstream https://github.com/kosmikus/lhs2tex/issues/104. I've also seen this pop up nondeterministically sometimes, and just adding empty lines invalidates some cache sufficiently...

Estimations: - collateral return output: 5 days - Forgo Reward Calculation Prefilter: this actually removes work - TxInfo Construction: unknown, probably quite large because it needs infrastructure

I could go either way on this. Both approaches have benefits and drawbacks, and to a large degree the original decision to go with LaTeX was just based on precedent....

> [@WhatisRT](https://github.com/WhatisRT) Thanks for outlining the pros of the status quo and how Markdown could improve the situation - I agree with your benefits listed. Can we make the pros...