Stream: Coq devs & plugin devs

Topic: Finding names used in a term

view this post on Zulip Li-yao (Feb 07 2021 at 19:50):

I'm trying to get better parameter names in the types of projections

I think all I have to do is to pick a binder name for the record that does not occur in the record declaration. How to get the set of bound names in a constr? Should that be just a loop using destProd? If I can do that then I figure that I can use Namegen.next_ident_away to get a fresh enough name.

If there's a better way to do all of that I'm all ears.

Last updated: Dec 07 2023 at 17:01 UTC