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

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

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