Add "of _ & _ & _" syntax

Author: proux01

doc/changelog/02-specification-language/21611-of-ampersand.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  new syntactic sugars `of T` and `& T` for anonymous binders
+  `(_ : T)`. In particular, this enables the
+  `Variant t := C1 of a & b & c | C2 of d.` syntax
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  by Pierre Roux).

doc/sphinx/addendum/generalized-rewriting.rst

@@ -176,7 +176,7 @@ These commands support the :attr:`local` and :attr:`global` locality attributes.
 The default is :attr:`local` if the command is used inside a section, :attr:`global` otherwise.
 They also support the :attr:`universes(polymorphic)` attributes.
 
-.. cmd::  Add Parametric Relation {* @binder } : @one_term__A @one_term__Aeq {? reflexivity proved by @one_term } {? symmetry proved by @one_term } {? transitivity proved by @one_term } as @ident
+.. cmd::  Add Parametric Relation @binders : @one_term__A @one_term__Aeq {? reflexivity proved by @one_term } {? symmetry proved by @one_term } {? transitivity proved by @one_term } as @ident
 
    Declares a parametric relation of :n:`@one_term__A`, which is a `Type`, say `T`, with
    :n:`@one_term__Aeq`, which is a relation on `T`, i.e. of type `(T -> T -> Prop)`.
@@ -235,7 +235,7 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism {* @binder } : @one_term with signature @term as @ident
+.. cmd:: Add Parametric Morphism @binders : @one_term with signature @term as @ident
 
    Declares a parametric morphism :n:`@one_term` of
    signature :n:`@term`.  The final identifier :token:`ident` gives a unique
@@ -777,7 +777,7 @@ Deprecated syntax and backward incompatibilities
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
 
-.. cmd:: Add Parametric Setoid {* @binder } : @one_term @one_term @one_term as @ident
+.. cmd:: Add Parametric Setoid @binders : @one_term @one_term @one_term as @ident
    :undocumented:
 
 .. cmd:: Add Morphism @one_term : @ident

doc/sphinx/addendum/type-classes.rst

@@ -289,7 +289,7 @@ Command summary
 ---------------
 
 .. cmd:: Class @record_definition
-         Class @ident_decl {* @binder } {? : @sort } := @constructor
+         Class @ident_decl @binders {? : @sort } := @constructor
 
    The first form declares a record and makes the record a typeclass with parameters
    :n:`{* @binder }` and the listed record fields.
@@ -344,7 +344,7 @@ Command summary
       or :n:`@constructor` with a right-hand-side that
       is not itself a Class has no effect (apart from emitting this warning).
 
-.. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_val } %} | := @term } }
+.. cmd:: Instance {? @ident_decl @binders } : @type {? @hint_info } {? {| := %{ {* @field_val } %} | := @term } }
 
    Declares a typeclass instance named :token:`ident_decl` of the typeclass
    :n:`@type` with the specified parameters and with
@@ -380,7 +380,7 @@ Command summary
       to fill them.  It works exactly as if no :term:`body` had been given and
       the :tacn:`refine` tactic has been used first.
 
-   .. cmd:: Declare Instance @ident_decl {* @binder } : @term {? @hint_info }
+   .. cmd:: Declare Instance @ident_decl @binders : @term {? @hint_info }
 
       In a :cmd:`Module Type`, declares that a corresponding concrete
       instance should exist in any implementation of this :cmd:`Module Type`. This

doc/sphinx/language/core/assumptions.rst

@@ -11,6 +11,10 @@ Binders
 .. prodn::
    open_binders ::= {+ @name } : @type
    | {+ @binder }
+   | @anon_binders
+   binders ::= {* @binder }
+   | {* @binder } @anon_binders
+   anon_binders ::= {| of | & } {+& @term99 }
    name ::= _
    | @ident
    binder ::= @name
@@ -38,6 +42,8 @@ variable can be introduced at the same time. It is also possible to give
 the type of the variable as follows:
 :n:`(@ident : @type := @term)`.
 
+`of T` and `& T` are syntactic sugar for anonymous binders `(_ : T)`.
+
 `(x : T | P)` is syntactic sugar for `(x : @Stdlib.Init.Specif.sig _ (fun x : T => P))`,
 which would more typically be written `(x : {x : T | P})`.
 Since `(x : T | P)` uses `sig` directly,

doc/sphinx/language/core/coinductive.rst

@@ -136,7 +136,7 @@ Co-recursive functions: cofix
 .. prodn::
    term_cofix ::= let cofix @cofix_body in @term
    | cofix @cofix_body {? {+ with @cofix_body } for @ident }
-   cofix_body ::= @ident {* @binder } {? : @type } := @term
+   cofix_body ::= @ident @binders {? : @type } := @term
 
 The expression
 ":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`"
@@ -154,7 +154,7 @@ Top-level definitions of corecursive functions
    .. insertprodn cofix_definition cofix_definition
 
    .. prodn::
-      cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations }
+      cofix_definition ::= @ident_decl @binders {? : @type } {? := @term } {? @decl_notations }
 
    This command introduces a method for constructing an infinite object of a
    coinductive type. For example, the stream containing all natural numbers can

doc/sphinx/language/core/definitions.rst

@@ -140,7 +140,7 @@ Assertions cause Rocq to enter :term:`proof mode` (see :ref:`proofhandling`).
 Common tactics are described in the :ref:`tactics` chapter.
 The basic assertion command is:
 
-.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type }
+.. cmd:: @thm_token @ident_decl @binders : @type {* with @ident_decl @binders : @type }
    :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property
 
    .. insertprodn thm_token thm_token

doc/sphinx/language/core/inductive.rst

@@ -31,8 +31,8 @@ Inductive types
    .. insertprodn inductive_definition constructor
 
    .. prodn::
-      inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
-      constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? @of_type_inst }
+      inductive_definition ::= @ident {? @cumul_univ_decl } @binders {? %| @binders } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
+      constructor ::= {* #[ {+, @attribute } ] } @ident @binders {? @of_type_inst }
 
    Defines one or more
    inductive types and its constructors.  Rocq generates

doc/sphinx/language/core/records.rst

@@ -21,11 +21,11 @@ Defining record types
    .. insertprodn record_definition of_type_inst
 
    .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {? {+; @record_field } {? ; } } %} {? as @ident } }
+      record_definition ::= {? > } @ident_decl @binders {? : @sort } {? := {? @ident } %{ {? {+; @record_field } {? ; } } %} {? as @ident } }
       record_field ::= {* #[ {+, @attribute } ] } @name {? @field_spec } {? %| @natural } {? @decl_notations }
-      field_spec ::= {* @binder } @of_type_inst
-      | {* @binder } := @term
-      | {* @binder } @of_type_inst := @term
+      field_spec ::= @binders @of_type_inst
+      | @binders @of_type_inst := @term
+      | @binders := @term
       of_type_inst ::= {| : | :> | :: | ::> } @type
 
    Defines a non-recursive record type, creating projections for each field
@@ -262,7 +262,7 @@ Constructing records
 
    .. prodn::
       term_record ::= %{%| {? {+; @field_val } {? ; } } %|%}
-      field_val ::= @qualid {* @binder } := @term
+      field_val ::= @qualid @binders := @term
 
    Instances of record types can be constructed using either *record form*
    (:n:`@term_record`, shown here) or *application form* (see :n:`@term_application`)

doc/sphinx/language/core/variants.rst

@@ -25,7 +25,7 @@ the type is a :gdef:`recursive type`, in which case it can be either
 is reserved for non-recursive types. Natural numbers, lists or streams cannot
 be defined using :cmd:`Variant`.
 
-.. cmd:: Variant @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
+.. cmd:: Variant @ident_decl @binders {? %| @binders } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
 
    Defines a variant type named :n:`@ident` (in :n:`@ident_decl`)
    with the given list of constructors.

doc/tools/docgram/common.edit_mlg

@@ -2298,7 +2298,6 @@ SPLICE: [
 
 | preident
 | lpar_id_coloneq
-| binders
 | check_module_types
 | decl_sep
 | function_fix_definition (* loses funind annotation *)