Jacques Carette
Jacques Carette
As I learn more, I'm thinking that QTT would be even better. Feels like it would subsume all the current erasability annotations and give linearity and more, all at once.
What if the 'proper' long normal form was `λ {record {l = l; r = r} → c l r}` instead ? Then everything is much more clearly linear. It...
I'm using pattern-matching lambda, as in ```agda postulate D : Set record XX : Set where constructor c field l : D r : D id : XX → XX...
For further progress on `stan`, maybe best to turn off those two suggestions for now? Certainly we shouldn't be relying on lazyness in a fundamental way, so if glassbr causes...
What is the state of this issue in general? Are `stan` and `weeder` part of our workflow, or still manual? (Not a complaint, looks like a lot of progress has...
Upon re-reading: yes.
Yes, it is redundant to have 'Chunk' in those names, and they should be renamed. Most of them should just have the `Chunk` part deleted. Some need renamed (`Constrained` stands...
You are correct that there seems to be a confusion in this example between `position` and `positionVec`. Your instincts are correct that `position` should not be used at all, and...
It does make sense to define the 'concept' of `position`; `positionVec` should, in theory, refer to that. But our current arrangement of Chunks may not really support that at the...
Amusingly in code that Conor and I are currently writing, we've gone in the opposite direction: we've generalized some cong-like functions to take that explicit proofs on the 'obvious input'...