|
|
|
|
|
|
by amenn
5 days ago
|
|
|
There's no wrong in vibe coding as long as you check what's the output. I can be wrong or missing the goal of course. But the work is in progress and I'm not writing a bash script for the theorem of pytagora. It's more complex and I'm studying as I go. You reviewed frontend/ast.ml, the small kernel, and concluded MLTT, but you missed frontend/cubical.ml. Thanks for the time you took to bring this critique, it will be helpful in the end. |
|
|
In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).
I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.
`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.