How does kernel conversion deal with let binders? (Is there a description of this part of the algorithm somewhere?)
Moved here, since I don't think you posted to #coqbot devs & users on purpose.
I've been looking into this quite a bit lately (though not related to
let). I'd be very interested if someone wants to discuss it.
My understanding is that conversion is done through the
fconstr type, and is entered (during type checking) through
The core of that algorithm lives in
eqappr, but I believe that the
let logic is taken care of in the actual reduction engine (inside
I believe, but I might be wrong about this one, that
usubs is the type of closure environment (delayed substitutions). These are substituted out when the term is converted back to a
yes, but conversion does not convert back to constr
There are places where it is converted to
constr during type checking. I've been looking into them when type checking applications
But you are right, it does not happen during conversion
Last updated: Dec 07 2023 at 09:01 UTC