🧊 Use forall_cof from Kado #362
Conversation
| let forall sym = | ||
| let i = Dim.DimProbe sym in | ||
| extend @@ | ||
| function |
There was a problem hiding this comment.
I am still a tiny bit concerned about the invariants here. But I do not have a counterexample... @favonia Can you perhaps explain why you are mostly certain this is OK?
There was a problem hiding this comment.
I believe I did not change the functionality of the code---that is, it is wrong iff it was wrong. Notice that there are two forall now---one is syntactic (cheap) and one is semantic (expensive), and it is the semantic (expensive) one used here. I am worried about the invariant but I was already worried before this PR. Does this answer your question?
There was a problem hiding this comment.
Where is the expensive one located now?
There was a problem hiding this comment.
The syntactic forall: https://redprl.org/kado/kado/Kado/Builder/Endo/module-type-S/index.html#val-forall
The semantic forall: https://redprl.org/kado/kado/Kado/Theory/Make/Disj/index.html#val-forall_cof
There was a problem hiding this comment.
Oh cool!! Sorry for my 🌰 🧠
There was a problem hiding this comment.
Where is the expensive one located now?
There was a problem hiding this comment.
Where is the expensive one located now?
Most relevant code (but I also changed other parts to make it work): https://github.com/RedPRL/kado/blob/b23ff87cfbaab6a5d35019f49da69227a252dcc6/src/Theory.ml#L392-L414
See RedPRL/kado#6.