Jon Sterling
Jon Sterling
This will be needed to satisfactorily implement #26 / #25. In particular, what I want is to be able to write something like `a : Univ such that under phi,...
I want to see if it is possible to make the nbe equality checker return a list of flex-flex and flex-rigid constraints which would make the equation true. Alternatively, a...
These are exactly the case that our direct computation rules cannot deal with (because it is not a stable reduction). Also, @favonia, what happens with HITs? do we generate typed...
The metalanguage has some very dope stuff, that I'd like to start explaining (as a basis for continuing to develop it and improve it, and eventually expose it to the...
Right now, this is a hodge-podge of useful functions, but it is hard to understand how to use them except by looking at examples. It would be helpful to close...
This operation should take every free symbol (basically, the operator ids) and rename it by some operation (such as a qualifying prefix like `fn x => "mylib#" ^ x`, etc.)....
For now, just a local library in this repository.
Maybe we shouldn't automatically unfold anything in evaluation, and instead rely on `Quote` to specifically request it during checking definitional equivalence. I think I see a way to make that...
@ecavallo I'd like to consider decomposing the eliminators into *two* different combinators: `case` and `rec`, as described in here: https://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf The idea is that `case` doesn't do any recursion, but...
Right now, `hcom,ghcom` violate this invariant. We would need to add `nghcom`.