Jason Gross

This one is somewhat longer: ``` 02:52:44.007 [info] Handle Execution of Cells 0 for /Interactive-1.interactive 02:52:44.008 [debug] Cell Index:0 sent to kernel 02:52:46.567 [debug] Interpreter for Pylance for Notebook URI...

Is there no backwards compatible fix? In any case, I'll update the compact machinery for 8.20, 9.0, 9.1

Oh, sorry, I was thinking this is a different pr. I'll go update the compat machinery

I've updated the infrastructure in https://github.com/mit-plv/fiat/commit/5b11e4b0f8e0e6bd3800f1b8148d59241fee4332, so writing an overlay should now be straightforward

Added v9.2 files in https://github.com/mit-plv/fiat/commit/21f4b81eb08ef5d7cebf6794b7adb63e9d05db03

Another reduction use case: - reducing PHOAS passes (must be fast, integrate with Qed, and have the ability to force normalization under lambdas before later applying them) --- currently my...

I have a pass that converts from PHOAS representation to de Bruijn representation and a pass that converts from de Bruijn representation to PHOAS, and I compose these passes to...

Good point, no closure necessary

For some reason I thought they were different, but thinking about it now, I think indeed these are just mkLambda / mkProd / mkLetIn for preterm.

I guess there is a subtlety in how shadowing of binders is dealt with. I believe in_context guarantees that the binder name given is the one used to refer to...