redtt
redtt copied to clipboard
RedPRL
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
When using generalization tactics, it's helpful to be able to hide the dummy hypotheses that were generalized away. Really there seems to be no actual reason to delete them; we...
This is today’s example of combinatorial explosion (the same issue is present in cubicaltt), which might be why we didn’t manage to compute pi_4(S^3) yet. Each test has twice as...
``` data unit where | triv opaque let t : (A : type) × A = (unit, triv) let a = t .snd ``` raises `Failure("popl: empty")`. Writing ``` let...
This will also make inductive types more awesome.
Maybe the ones without valid systems can made Kan with ghcom? Moreover, the validity of the system in an Ext type is stable under substitutions, and so we can just...
This is something that was first noticed by favonia a while back, but I wanted to write it down so that we can theorize a fix. A diagonal dimension action...
As far as I understand, Agda's (idealized) core type theory has only top-level definitions, rather than allowing an eliminator to be applied at any point in the program. This doesn't...