another bit that tripped me up for a long time was that my constraint solver is no longer just doing unification, it’s computing judgemental equality, and hence also normalization, evaluation under binders, etc. much larger scope.
Conversation
Ohh, this is all really helpful! Might take me a while to unpack - I haven't gone as deep as you, but it rings many bells from looking at 's elaboration-zoo a while back. It's super handy to have some of these problems stated explicitly in this way though!
2
2
Yeah for sure - at the moment I've been mainly cargo-culting off the elaboration-zoo, but it's sometimes hard to understand _why_ certain choices where made, and what the other options are. I also find papers on unification rather hard to break the ice on. 😬
3
1
I always value the time others have put into this stuff, and want to learn as much as possible from those struggles, even if there's only so much that I can get my head around at a time! So your experience is super valuable to me! 🙂
1
3
1
3
additionally, we are told that the IRC crowd miss you. won't try to hard-sell it, but thought we'd mention.
1
1
Aww thanks - bit tired now tbh - I'll try to get it working - if not today, maybe tomorrow! Would be handy to have that Matrix IRC bridge at any rate. 🙂
Ok, managed to join at last! haha!
1
Show replies