Reed Mullanix
Reed Mullanix
## Issue Description There's an error somewhere that leads to an off-by-one error in some DeBruijin Arithmetic, leading to invalid printing or segfaults.
# Description There are a couple of places in the 1Lab where we manually eta-expand out copattern definitions by hand to get better goal display. This mostly comes up when...
# Description This PR reworks the simplex category to make it more amenable to defining diagrams. It also proves a whole host of properties about it, which required the introduction...
I often use `-fdefer-type-errors` when using `haskell-interactive-mode`, as it lets me load files and get things like type at point, goto-defn, etc, even when there are type errors. However, it...
When dealing with program refinement (or really any domain with the notion of a meta-variable), capturing substitution is required. For example, consider the language and judgements below. ``` e ::=...
# Patch Description This PR adds type holes, as well as some error reporting infrastructure. Such is life when we start a new proof assistant, hard to work on one...
The pretty printer right now is pretty bad! I should be able to use the ordered hash map in place of the crummy pretty printer environment, which should get rid...
It would be a good idea to add natural numbers for some nice meta programming examples. Shouldn't be too hard?
It would be a good idea to add some example configurations for various editors, so we could just copy+paste when using `asai.lsp` in other projects. Unfortunately, the situation with `lsp-mode`...