Stream: Coq devs & plugin devs

Topic: `let` binders and kernel conversion


view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:22):

Moved here, since I don't think you posted to #coqbot devs & users on purpose.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Oct 05 2022 at 05:10):

yes, but conversion does not convert back to constr

view this post on Zulip 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

view this post on Zulip Gregory Malecha (Oct 05 2022 at 11:24):

But you are right, it does not happen during conversion


Last updated: Oct 13 2024 at 01:02 UTC