Recent roadmap

[ice1000]

0. (@wsx-ucb) lazy term visitor (Lazy Term visitor #356), including subst and ulift reimplementation (The ability to lift a meta #352)
1. (unassigned, probably @ice1000) completely replace core term visitors with lazy term visitor (Completely remove visitors everywhere? #315)
2. (@ice1000) reimplement cubical features, replace conditions with cubical boundaries, remove records with conditions (future branch)
3. (@tsao-chi) reimplement structs (in par with above)
4. (@lunalunaa) term-with-hole based tactics (in par with above)

For 3, I suggest getting started once records w/ conditions are removed. You may base your work on my WIP branch (future), I haven't removed them for now

[ice1000]

0 should be finished asap, because it essentially blocks everything. Then, I'll try to remove records w/ conditions and redefine the path type using the redtt syntax. This should be quick and should unblock every other task. I'll try to reimplement HIT at the same time everyone else do their things.

[ice1000]

We have finished 0-2!