From 5249611d75c18e449c19cb8eaa071d00c3347e44 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 3 Nov 2022 10:07:38 +0100 Subject: [PATCH] doc: fix `mkAntiquot` docstring --- src/Lean/Parser/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 24fd380ecd..1d393e9436 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1750,8 +1750,8 @@ def unicodeSymbol (sym asciiSym : String) : Parser := tokenWithAntiquot (unicodeSymbolNoAntiquot sym asciiSym) /-- - Define parser for `$e` (if anonymous == true) and `$e:name`. - `kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is false. + Define parser for `$e` (if `anonymous == true`) and `$e:name`. + `kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is true. Antiquotations can be escaped as in `$$e`, which produces the syntax tree for `$e`. -/ def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser := let kind := kind ++ (if isPseudoKind then `pseudo else Name.anonymous) ++ `antiquot