Andre Knispel
Andre Knispel
It would be great to support pattern matching in the conclusion of a rule, to avoid having to write a bunch of `let`'s and explicit binders at the beginning of...
We need to deal with branching. We should be able to turn a proof that only at most one constructor applies into an instance of `Computational`. This means that we'd...
The current computation strategy is incompatible with nested rules. To fix this, instead of having clauses return a boolean, we can have them return a `Maybe X`, and do a...
All elements in the `UMap` need to have a deposit & reward amount. So the half of the constructors that don't have that should be unused. Also, Conway removes pointer...
Here's a literate Agda file that LaTeX doesn't like: ``` \documentclass{article} \usepackage{agda} \begin{document} \begin{AgdaMultiCode} \begin{code} module Latex-Bug where open import Data.Bool open import Function ff : Bool ff = true...
This was requested by Thorsten at the current AIM, and I find this useful myself. I'd be happy to add defaults for other modes as well, but there was a...
This is part of upstreaming properties that seem generally useful.
Upstreaming some functions that I've used to prove things about sets (not the Agda kind).
Those governance actions that cannot cause a script to run on proposal should prevent that proposal from being supplied. There should be a check next to `∙ (∃[ u ]...
- [ ] `genErrors` always generates fully qualified names. The output would be a lot more readable if we postprocess the string to remove those qualifiers. - [ ] We...