Documentation

Mathlib.Tactic.FindSyntax

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.

source
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.

Equations
Instances For
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For