The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Sun, 13 Jun 2021 12:03:01 -0700
Jim Fehrle <jim.fehrle AT gmail.com> wrote:

> Some clues:
> The ">" corresponds to the non-terminal "opt_coercion".  The text
> describing "record_definition" in the doc describes how that works for
> records.
> 
> [image: image.png]


That doc says:

> If provided, the constructor name is automatically declared as a
> coercion from the class of the last field type to the record name
> (this may fail if the uniform inheritance condition is not
> satisfied). 

That does not seem like it would add additional behavior for a singleton
Class.   A singleton class will already act as though there is a
coercion from the field to the class, because the field is not wrapped
in a record, and no constructor is needed.

Parameter T : Type.
Parameter a : T.

Class Foo := foo:T.

Definition f := let x:Foo := a in x. (*succeeds*)
Eval vm_compute in f. (*evaluates to a*)

Substituting record for class:

Record Foo := {foo:T}.

fails in the definition of f, but

Record >Foo := {foo:T}.

succeeds.  So the leading ">" seems useful for records, but not for
singleton classes.  Interestingly, it might be useful for classes that
are record definitions, but it doesn't work:

Class >Foo := {foo:T}.

is allowed, but fails in the definition of f above.

BTW: I'm testing this in 8.13.2.