In nbe-for-mltt, why do you only add a definition to the environment when evaluating lambdas, but not for the other binders, like pi types and sigma types? github.com/jozefg/nbe-for
Conversation
Found this when trying to track down a binding bug in my code when I try to implement elaboration into a fully annotated core syntax, and it would be nice to understand. I'm having to do a readback for the annotations on lambdas though which is kind of frustrating :/
Replying to
Oh wait, I think I get it - the argument is added to the environment in `do_clos` and `do_clos2`: github.com/jozefg/nbe-for
1