max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix mkAntiquot docstring

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-03 10:07:38 +01:00
parent 17d67bb24c
commit 5249611d75
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Basic.lean
View file

@ -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