Add & T syntax for anonymous binders (_ : T)

Author: proux01

dev/ci/user-overlays/21611-proux01-of-ampersand.sh

@@ -0,0 +1,7 @@
+overlay analysis https://github.com/proux01/analysis rocq21611 21611
+overlay deriving https://github.com/proux01/deriving rocq21611 21611
+overlay fcsl_pcm https://github.com/proux01/fcsl-pcm rocq21611 21611
+overlay finmap https://github.com/proux01/finmap rocq21611 21611
+overlay mathcomp https://github.com/proux01/math-comp rocq21611 21611
+overlay mtac2 https://github.com/proux01/Mtac2 rocq21611 21611
+overlay oddorder https://github.com/proux01/odd-order rocq21611 21611

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

@@ -1,6 +1,6 @@
 - **Added:**
-  new syntactic sugars `of T & ... & T` for anonymous binders
-  `(_ : T)` in constructors, enabling the
+  new syntactic sugars `& T` for anonymous binders `(_ : T)`
+  and `of T & ... & T` for anonymous binders in constructors, enabling the
   `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax.
   This adds the new reserved keyword `of`
   (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,

doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst

@@ -0,0 +1,5 @@
+- **Removed:**
+  the `of T` syntax for anonymous binders outside of constructors,
+  use `& T` instead
+  (`#21611 <https://github.com/rocq-prover/rocq/pull/21611>`_,
+  by Pierre Roux).

doc/sphinx/language/core/assumptions.rst

@@ -20,6 +20,7 @@ Binders
    | @generalizing_binder
    | ( @name : @type %| @term )
    | ' @pattern0
+   | & @term99
 
 Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix`
 *bind* variables. A binding is represented by an identifier. If the binding
@@ -38,6 +39,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)`.
 
+:n:`& @term99` is syntactic sugar for the anonymous binder :n:`(_ : @term99)`.
+
 `(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/tools/docgram/fullGrammar

@@ -348,6 +348,7 @@ closed_binder: [
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
+| "&" term99
 ]
 
 one_open_binder: [

doc/tools/docgram/orderedGrammar

@@ -405,6 +405,7 @@ binder: [
 | generalizing_binder
 | "(" name ":" type "|" term ")"
 | "'" pattern0
+| "&" term99
 ]
 
 implicit_binders: [

parsing/g_constr.mlg

@@ -508,7 +508,9 @@ GRAMMAR EXTEND Gram
         { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (MaxImplicit, b), t)) tc }
       | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (NonMaxImplicit, b), t)) tc }
-      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
+      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] }
+      | "&"; c = term LEVEL "99" ->
+        { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] } ] ]
   ;
   one_open_binder:
     [ [ na = name -> { (pat_of_name na, Explicit) }

plugins/ssr/ssrvernac.mlg

@@ -116,14 +116,6 @@ GRAMMAR EXTEND Gram
   ] ];
 END
 
-GRAMMAR EXTEND Gram
-  GLOBAL: closed_binder;
-  closed_binder: TOP [
-    [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
-      { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] }
-  ] ];
-END
-
 (** Vernacular commands: Prenex Implicits *)
 
 (* This should really be implemented as an extension to the implicit   *)

test-suite/prerequisite/ssr_mini_mathcomp.v

@@ -695,7 +695,7 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
@@ -798,7 +798,7 @@ Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
@@ -948,7 +948,7 @@ Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c T.
+Definition clone c & phant_id class c := @Pack T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 

theories/Corelib/ssr/ssreflect.v

@@ -231,7 +231,7 @@ Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put.
 
 Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
 
-Definition get_by vT sT of sT -> vT := @get vT sT.
+Definition get_by vT sT & sT -> vT := @get vT sT.
 
 End TheCanonical.