Stream: Coq users

Topic: Record variable name

view this post on Zulip Li-yao (Dec 29 2020 at 21:45):

Apparently when I define a record, the first letter of the type is used as the name of the record in the types of the projection. For example,

Record Adjunction :=
  { unit : forall {a}, a }.

About unit.

I get unit : Adjunction -> forall a0, a0 whereas I expected unit : Adjunction -> forall a, a, I assume that's to avoid shadowing the first argument unit : forall (a : Adjunction) (a0 : Type), a0 (which is relevant when the fields depend on each other).

I can use Arguments to rename the arguments of the projection, but if there are many projections, is there a shorter way? Isn't there some way, when a type is defined, to choose the default letter for variables of that type and avoid the name clash in the first place?

view this post on Zulip Matthieu Sozeau (Jan 06 2021 at 13:53):

There should be, it's not available in the user-level syntax AFAIK.

Last updated: Sep 26 2023 at 13:01 UTC