redtt
redtt copied to clipboard
RedPRL
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
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...
- [ ] cache the locations of redlib files. - [x] unify the API for data declarations and normal declarations. - [x] unify the tags in GlobalEnv and ResEnv. -...
This is after #418. The analogy is to treat the current file system as partitions on a disk, and we are building a virtual file system on top of them....
Right now, `hcom,ghcom` violate this invariant. We would need to add `nghcom`.
Although this is not crucial, I could not figure out _why_ it does not work as it is. The current Vim highlighting fails to highlight `def` in the following case:...
I think it would be cool to write ``` Cx.ext_dim blah... @@ fun x -> Cx.ext_ty foo... @@ fun y -> Cx.def hey... @@ cx ```