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 https://github.com/coq/coq/issues/13727

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: Oct 16 2021 at 07:02 UTC