Running into an issue with my elaborator. It seems that I get lots of bloated definition when I elaborate to my core syntax - seemingly because `synth_term` unfolds variables to their definitions a bit too eagerly. Was wondering if you had any tips! cc.
Conversation
This is the main part that does the work of elaborating items: github.com/brendanzab/rus - I'm thinking it might be worth limiting the the `read_back_value` line to lookup variables in my implementation of nbe?
Replying to
I guess I'm already elaborating to variables during synthesis, so that shouldn't be the issue here: github.com/brendanzab/rus
Replying to
So you want to weaken forward declared types to the scope of their definitions. Readback is not good because you don't want normal forms in elab output. I can think of several solutions varying in simplicity and generality.
1
1
a) Implement weakening directly on core syntax, store plain elaborated types in forward_declarations, weaken them as needed. This is pretty efficient because you only need to weaken each forward declared type once.
1
1
Show replies