Andre Knispel

That's right, the big issue here is that we don't yet have support for multiple versions in the spec. There are a few more pressing issues and challenges associated with...

I don't know the planned timelines, so I'm not entirely sure. There'll probably be a push to get as many items as possible ironed out before the launch once we...

Closing this - the original issue has been closed and I don't know if it's even relevant anymore

Since we don't have Babbage yet, we can't really do any work on this. There's also no urgency at all, so we can revisit this at some unknown later point.

I think your initial thought that it's not computational is correct, since if there are multiple options for `canVote` the `compute` function could be a `just` or a `nothing` depending...

Now that you've implemented it, obviously this is `Computational`. Just to remember this in the future, since the hash of a transaction goes into the `aid`, there won't be any...

Since we've recently had issues with memory allocation, it would also be nice to include an output of the GHC memory statistics.

For reference, here's one way how to do quotients in `--erased-cubical`: ``` agda {-# OPTIONS --safe --erased-cubical #-} module Quotients where open import Agda.Builtin.Cubical.Path open import Agda.Primitive.Cubical record Quotient (A...

Yeah, I think this is something for next year when we have more breathing room. Also, I realized that we can't import `Relation.Binary.PropositionalEquality` with `--erased-cubical`, so taking this route would...

Just to be sure, your plan is to make something akin to `List-Model` in `Axiom.Set.List`, correct? Note that this won't admit instances of `Theoryᶠ` and `Theoryᵈ`, which are both necessary...