Andre Knispel
Andre Knispel
There are some things that would be nice to eventually have in CI: - [x] cached builds (should make running CI significantly faster) - [ ] mac builds - [x]...
The current MA implementation is still missing a few things, in particular: - [x] One or more implementations of the `Value` type (Fig. 3) - [ ] Adjusting `scriptsNeeded` to...
Tactics that call themselves recursively usually rely on some fuel value. Currently, all of this is quite ad-hoc and difficult to use. In particular there are two problems: - [...
A zipped transaction is one where all the pointers to information have been properly resolved. Currently it's not possible to zip a transaction without any extra information. We've been considering...
We have many properties for which we need decidability. It would make sense to look into deriving that automatically.
The derivation strategy is currently quite slow. In particular, I've noticed that printing contexts at the start of a computation is pretty much instant, while it sometimes takes multiple seconds...
1. The tactics such as `∈⇔P` are pretty nice, but there is of course the issue that we have to copy&paste it everywhere. Maybe there's some solution that doesn't require...
We want to use set comprehension to write sets and maps. There are some difficulties: - The syntax keyword isn't powerful enough, but we could for example have a notation...
We currently just put the literate (LaTeX) Agda in the HTML output, which produces a bunch of garbage. It would be nice to have good-looking HTML output as well, but...