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

doc: fix categoryParenthesizer documentation

Browse source
This commit is contained in:
Mario Carneiro 2021-07-15 00:39:28 -07:00 • committed by GitHub
parent 93a3fd14ad
commit 8d616e060b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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/PrettyPrinter/Parenthesizer.lean
View file

@ -137,7 +137,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa
name := `categoryParenthesizer,
descr := "Register a parenthesizer for a syntax category.
[parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`,
[categoryParenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`,
which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize`
with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized,
but still be traversed for parenthesizing nested categories.",
@ -146,7 +146,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa
let env ← getEnv
let id ← Attribute.Builtin.getId stx
if Parser.isParserCategory env id then pure id
else throwError "invalid [parenthesizer] argument, unknown parser category '{toString id}'"
else throwError "invalid [categoryParenthesizer] argument, unknown parser category '{toString id}'"
} `Lean.PrettyPrinter.categoryParenthesizerAttribute
@[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer