redtt
redtt copied to clipboard
RedPRL
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
The eliminator for a HIT takes `fhcom`s to `com`s in the target type. When the motive is non-dependent, the output `com` is in a constant line, so the desired behavior...
What I don't like about the current unification algorithm is that by restricting the pattern fragment to things applied to spines of variables, we end up needing to do a...
There are some strange spaces that I could not understand in the printed expressions.
Lean has a really nice feature where names are hierarchical, so a single declaration `foo` might elaborate such that `foo` has a meaning, but also `foo.x` and `foo.y` etc. have...
I want a hole to be able to range over a suffix to the spine. While we support interactive backward construction already, this would enable interactive *forward* construction.
It would be nice to print holes using the source language rather than the core language by default, since users shouldn't be expected to understand the intricacies of the core....
Before I forgot some good (?) marketing strategies...