Quelle  attributes.out   Sprache: unbekannt

Rocq < Toplevel input, characters 17-29:
> #[canonical=yes, canonical=no] Definition a := 3.
>                  ^^^^^^^^^^^^
Error: Attribute for canonical specified twice.

Rocq < Rocq < Toplevel input, characters 29-43:
> #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
>                             ^^^^^^^^^^^^^^
Error: key 'polymorphic' has been already set.

Rocq < Rocq < Toplevel input, characters 13-28:
> #[universes(polymorphic=foo)] Definition a := 3.
>             ^^^^^^^^^^^^^^^
Error: Invalid value 'foo' for key polymorphic
use one of {yes, no}

Rocq < Rocq < Toplevel input, characters 13-29:
> #[universes(polymorphic(foo))] Definition a := 3.
>             ^^^^^^^^^^^^^^^^
Error: Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.

Rocq < Rocq < Toplevel input, characters 13-33:
> #[universes(polymorphic(foo,bar))] Definition a := 3.
>             ^^^^^^^^^^^^^^^^^^^^
Error: Invalid syntax polymorphic(foo, bar), try polymorphic={yes,
no} instead.

Rocq < Rocq < Toplevel input, characters 30-37:
> #[universes(polymorphic=yes, bla=bla)] Definition a := 3.
>                              ^^^^^^^
Error: This command does not support this attribute: universes.
[unsupported-attributes,parsing,default]

Rocq <