Stream: Coq devs & plugin devs

Topic: API to expand a primitive projction


view this post on Zulip Enrico Tassi (Nov 27 2020 at 10:20):

It's a big unusual, I know, but I'd like to take a compact primitive projection and expand it to the compatibility constant. Is there an API for that?
I did find Projection.constant to find a regular projection and Projction.npars which tells me how many missing parameters are there, but no API that also retypechecks the argument, finds the nparams parameters, and builds the regular application. Does is exist already? CC @Matthieu Sozeau

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:21):

Retyping.expand_projection?

view this post on Zulip Matthieu Sozeau (Nov 27 2020 at 10:22):

Look for expand_projection

view this post on Zulip Enrico Tassi (Nov 27 2020 at 10:28):

It was too obvious, for once ;-)


Last updated: Dec 06 2023 at 13:01 UTC