feat: update namedPattern parser

src/Init/Prelude.lean

@@ -170,7 +170,9 @@ structure Subtype {α : Sort u} (p : α → Prop) where
 /-- Auxiliary Declaration used to implement the notation (a : α) -/
 @[reducible] def typedExpr (α : Sort u) (a : α) : α := a
 
-/-- Auxiliary Declaration used to implement the named patterns `x@p` -/
+/-- Auxiliary Declaration used to implement the named patterns `x@p`
+    -- TODO: add proof for `x = a`
+-/
 @[reducible] def namedPattern {α : Sort u} (x a : α) : α := a
 
 /- Auxiliary axiom used to implement `sorry`. -/

src/Lean/Elab/Match.lean

@@ -493,7 +493,8 @@ partial def main (e : Expr) : M Pattern := do
     | some (α, lits) =>
       return Pattern.arrayLit α (← lits.mapM main)
     | none =>
-      if e.isAppOfArity `namedPattern 3 then
+      -- TODO: namedPattern will have 4 arguments
+      if e.isAppOfArity ``_root_.namedPattern 3 then
         let p ← main <| e.getArg! 2
         match e.getArg! 1 with
         | Expr.fvar fvarId _ => return Pattern.as fvarId p

src/Lean/Elab/PatternVar.lean

@@ -201,10 +201,14 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     processCtor stx[0]
   else if k == ``Lean.Parser.Term.namedPattern then
     /- Recall that
-      def namedPattern := check... >> trailing_parser "@" >> termParser -/
+      ```
+      def namedPattern := check... >> trailing_parser "@" >> optional (atomic (ident >> ":")) >> termParser
+      ```
+      TODO: pattern variable for equality proof
+     -/
     let id := stx[0]
     discard <| processVar id
-    let pat := stx[2]
+    let pat := stx[3]
     let pat ← collect pat
     `(_root_.namedPattern $id $pat)
   else if k == ``Lean.Parser.Term.binop then

src/Lean/Meta/Match/Basic.lean

@@ -15,6 +15,7 @@ inductive Pattern : Type where
   | ctor         (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern) : Pattern
   | val          (e : Expr) : Pattern
   | arrayLit     (type : Expr) (xs : List Pattern) : Pattern
+  -- TODO: add case for equality
   | as           (varId : FVarId) (p : Pattern) : Pattern
   deriving Inhabited
 
@@ -42,6 +43,7 @@ where
     | var fvarId                     => pure $ mkFVar fvarId
     | val e                          => pure e
     | as fvarId p                    =>
+      -- TODO
       if annotate then
         mkAppM `namedPattern #[mkFVar fvarId, (← visit p)]
       else
@@ -275,7 +277,8 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
     | some (α, lits) =>
       return Pattern.arrayLit α (← lits.mapM toPattern)
     | none =>
-      if e.isAppOfArity `namedPattern 3 then
+      -- TODO: `namedPattern` will have 4 arguments
+      if e.isAppOfArity ``namedPattern 3 then
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1 with
         | Expr.fvar fvarId _ => return Pattern.as fvarId p

src/Lean/Parser/Term.lean

@@ -265,7 +265,7 @@ def isIdent (stx : Syntax) : Bool :=
   stx.isAntiquot || stx.isIdent
 
 @[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
-@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
+@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
 
 @[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
 @[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."