feat: support dotted notation and named arguments in patterns

RELEASES.md

@@ -1,6 +1,14 @@
 Unreleased
 ---------
 
+* Support dotted notation and named arguments in patterns. Example:
+  ```lean
+  def getForallBinderType (e : Expr) : Expr :=
+    match e with
+    | .forallE (binderType := type) .. => type
+    | _ => panic! "forall expected"
+  ```
+
 * "jump-to-definition" now works for function names embedded in the following attributes
   `@[implementedBy funName]`, `@[tactic parserName]`, `@[termElab parserName]`, `@[commandElab parserName]`,
   `@[builtinTactic parserName]`, `@[builtinTermElab parserName]`, and `@[builtinCommandElab parserName]`.

src/Lean/Elab/PatternVar.lean

@@ -219,12 +219,13 @@ where
   processCtorApp (stx : Syntax) : M Syntax := do
     let (f, namedArgs, args, ellipsis) ← expandApp stx true
     if f.getKind == ``Parser.Term.dotIdent then
-      unless namedArgs.isEmpty do
-        throwError "invalid dotted notation in a pattern, named arguments are not supported yet"
+      let namedArgsNew ← namedArgs.mapM fun
+        | { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(mkIdentFrom ref name) := $(← collect arg)))
+        | _ => unreachable!
       let mut argsNew ← args.mapM fun | Arg.stx arg => collect arg | _ => unreachable!
       if ellipsis then
         argsNew := argsNew.push (mkNode ``Parser.Term.ellipsis #[mkAtomFrom stx ".."])
-      return Syntax.mkApp f argsNew
+      return Syntax.mkApp f (namedArgsNew ++ argsNew)
     else
       processCtorAppCore f namedArgs args ellipsis
 

tests/lean/run/dottedCtorNamedArgPattern.lean

@@ -0,0 +1,17 @@
+import Lean
+
+def f (x : Nat × Nat) :=
+  match x with
+  | .mk (snd := snd) .. => snd
+
+example : f (10, 20) = 20 := rfl
+
+open Lean
+def g (e : Expr) : Expr :=
+  match e with
+  | .forallE (binderType := type) .. => type
+  | e => e
+
+def h (x : Nat × Nat) :=
+  match x with
+  | .mk (α := .(Nat)) (snd := snd) .. => snd