The #find_syntax command

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, by inspecting the ParserDescriptor of the corresponding parser.

def Mathlib.FindSyntax.extractSymbols : Lean.ParserDescr → Array String → Array String

extractSymbols descr acc takes as input a ParserDescriptor descr and an accumulator array acc. It accumulates all symbols in descr corresponding to Lean.ParserDescr.symbol, Lean.ParserDescr.nonReservedSymbol or Lean.ParserDescr.unicodeSymbol.

The output array serves as a way of regenerating what the syntax tree of the input parser is.

def Mathlib.FindSyntax.«command#find_syntax_Approx» : Lean.ParserDescr

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.