How does kernel conversion deal with let binders? (Is there a description of this part of the algorithm somewhere?)
(context: https://github.com/coq/coq/issues/16606)
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 conv_leq
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 cClosure.ml
)
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 constr
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: Oct 13 2024 at 01:02 UTC