Li-yao (Feb 07 2021 at 19:50): 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: Sep 09 2024 at 05:02 UTC