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 Expression tree of the corresponding parser.

def Mathlib.FindSyntax.extractSymbols : Lean.Expr → Array Lean.Expr

extractSymbols expr takes as input an Expression expr, assuming that it is the value of a "parser". It returns the array of all subterms of expr that are the Expr.lit argument to Lean.ParserDescr.symbol and Lean.ParserDescr.nonReservedSymbol applications.

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

def Mathlib.FindSyntax.litToString : Lean.Expr → String

litToString expr converts the input Expression expr into the "natural" string that it corresponds to, in case expr is a String/Nat-literal, returning the empty string "" otherwise.

Equations

• Mathlib.FindSyntax.litToString (Lean.Expr.lit (Lean.Literal.natVal v)) = toString "" ++ toString v ++ toString ""
• Mathlib.FindSyntax.litToString (Lean.Expr.lit (Lean.Literal.strVal v)) = v
• Mathlib.FindSyntax.litToString x✝ = ""

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.