3e4fa12c72
This PR adds a `pp.unicode` option and a `unicode("→", "->")` syntax
description alias for the lower-level `unicodeSymbol "→" "->"` parser.
The syntax is added to the `notation` command as well. When `pp.unicode`
is true (the default) then the first form is used when pretty printing,
and otherwise the second ASCII form is used. A variant, `unicode("→",
"->", preserveForPP)` causes the `->` form to be preferred; delaborators
can insert `→` directly into the syntax, which will be pretty printed
as-is; this allows notations like `fun` to use custom options such as
`pp.unicode.fun` to opt into the unicode form when pretty printing.
Additionally:
- Adds more documentation for the `symbol` and `nonReservedSymbol`
parser descriptions.
- Adds documentation for the
`infix`/`infixr`/`infixl`/`prefix`/`postfix` commands.
- The parenthesizers for symbols are improved to backtrack if the atom
doesn't match.
- Fixes a bug where `&"..."` symbols aren't validated.
This is partial progress for issue #1056. What remains is enabling
`unicode(...)` for mixfix commands and then making use of it for core
notation.
|
||
|---|---|---|
| .. | ||
| Tactic | ||
| Term | ||
| Attr.lean | ||
| Basic.lean | ||
| Command.lean | ||
| Do.lean | ||
| Extension.lean | ||
| Extra.lean | ||
| Level.lean | ||
| Module.lean | ||
| StrInterpolation.lean | ||
| Syntax.lean | ||
| Tactic.lean | ||
| Term.lean | ||
| Types.lean | ||