From 430f4d28e49574911395b994167eadbd3ca6eb5d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Dec 2023 18:58:14 +0000 Subject: [PATCH] doc: mention `x:h@e` variant in docstring of `x@e` (#3073) This was done in 1c1e6d79a78597995cd96ab7725b63b461db7674 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Naming.20equality.20hypothesis.20in.20match.20branch/near/408016140) --- src/Lean/Elab/PatternVar.lean | 1 - src/Lean/Parser/Term.lean | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 29854a4ed4..800ae7c79c 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -146,7 +146,6 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc ``` def namedPattern := check... >> trailing_parser "@" >> optional (atomic (ident >> ":")) >> termParser ``` - TODO: pattern variable for equality proof -/ let id := stx[0] discard <| processVar id diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 1d79f4ab1b..3349d34185 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -669,7 +669,8 @@ def isIdent (stx : Syntax) : Bool := checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}" -/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/ +/-- `x@e` or `x:h@e` matches the pattern `e` and binds its value to the identifier `x`. +If present, the identifier `h` is bound to a proof of `x = e`. -/ @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >>