Andre Knispel

Thank you for writing this up! It seems like you'd vote for putting in the extra effort to get something like this: https://1lab.dev/Algebra.Monoid.html The different levels of detail might be...

I think this is most likely either a translation bug or a bug in `isRegistered` (though that looks fine to me right now). It's probably not a bug with registering...

It turns out that this is unrelated to the existential after all. Here's a minimized reproducer: ```agda open import Prelude test : String test = case (0 ≟ 1) ,′...

Ah, the documentation I wrote helpfully immediately reveals the bug: ``` -- genError: returns the type of the most recently bound variable as a string ``` So `genErrors` does all...

I don't think anything actually needs to change here. Assume `CommitteeMaxTermLength = 1`, and we're at epoch `e`. Then, if you make a proposal with term `e+2` and it gets...

The name of this parameter is somewhat inconsistent. I can find at least `maxBlockSize`, `maxBBSize` and `maxBlockBodySize`. For `maxHeaderSize`, I can also find `maxBHSize` which makes me think that a...

With these types of things I wonder if it'd be a good idea to implement some granularity for predicate failures. I.e. ones that affect block validation and ones that trigger...

Done

Naively I'd expect a hole to be treated like a postulate in this case. It is already a common occurrence in day-to-day development that filling in a hole "unsolves" constraints,...

I agree it's a bit messy, but I'm not sure how to do better here...