redtt

redtt copied to clipboard

Concrete notation of coe sucks!

3

Can we think of a better notation? It's so ugly. Honestly, comp is bad too when it is dependent.

jonsterling

Noticed this with @kaonn today; I'll try and troubleshoot & fix

jonsterling

Find a way to implement strict composition

5

``` import path import J data vacu where | more (x : vacu) let Code (m : vacu) (n : vacu) : type = elim n [ more n' =>...

ecavallo

Non-trivial argument types in CITs

6

Right now, the only kind of "argument type" allowed is just `Self`; this should be generalized to `A -> Self`, where `A` is a type. Combining this with #200, the...

jonsterling

There's a very subtle substitution bug that could potentially be triggered (but none of our examples did). This will be fixed in #270. Technical details: in the last rule on...

favonia

Non-local validity

3

The following should be valid, but it requires non-local reasoning: ``` comp x 1 blah [x=0 -> refl | z=0 -> \ y -> comp x y bar [x=0 ->...

favonia

[Efficiency] simultaneous, delayed substitution

1

AFTER #270.

favonia

Let equate_ty (quote_ty, equiv_ty) handle the types directly

3

This WILL be done in #270 unless @jonsterling says no.

favonia

Remove mortality in the coe of extension types

1

The following line is always a no-op. https://github.com/RedPRL/redtt/blob/9392635a6c7dcb7b3afddab8ef5210308426ea36/src/core/Val.ml#L1716 This is fixed in #270, but I want to document this.

favonia

The current structure will populate different instances of PersistentTable all over the places, and it is very possible that the expensive `reroot` will be called too many times. Therefore we...

favonia