Lean4
/-- The `#find_syntax` command takes as input a string `str` and retrieves from the environment
all the candidates for `syntax` terms that contain the string `str`.
It also makes a very crude effort at regenerating what the syntax looks like:
this is supposed to be just indicative of what the syntax may look like, but there is no
guarantee or expectation of correctness.
The optional trailing `approx`, as in `#find_syntax "∘" approx`, is only intended to make tests
more stable: rather than outputting the exact count of the overall number of existing syntax
declarations, it returns its round-down to the previous multiple of 100.
-/
@[command_parser 1000]
public meta def «command#find_syntax_Approx» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.FindSyntax.«command#find_syntax_Approx» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#find_syntax ") (ParserDescr.const✝ `str))
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " approx" false✝)))
