Jason Gross (Oct 04 2022 at 05:46): Jason Gross (Oct 04 2022 at 05:46):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)
Théo Zimmermann (Oct 04 2022 at 07:22):Moved here, since I don't think you posted to #coqbot devs & users on purpose.
Gregory Malecha (Oct 04 2022 at 23:20):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.
Gregory Malecha (Oct 04 2022 at 23:21):My understanding is that conversion is done through the fconstr type, and is entered (during type checking) through conv_leq
Gregory Malecha (Oct 04 2022 at 23:23):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)
Gregory Malecha (Oct 04 2022 at 23:41):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
Gaëtan Gilbert (Oct 05 2022 at 05:10):yes, but conversion does not convert back to constr
Gregory Malecha (Oct 05 2022 at 11:24):There are places where it is converted to constr during type checking. I've been looking into them when type checking applications
Gregory Malecha (Oct 05 2022 at 11:24):But you are right, it does not happen during conversion
Last updated: Apr 19 2024 at 09:01 UTC