Documentation

Lean.Elab.Quotation.Util

source
opaque Lean.Elab.Term.Quotation.hygiene :
Lean.Option Bool
source
def Lean.Elab.Term.Quotation.getAntiquotationIds (stx : Syntax) :
TermElabM (Array Ident)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Lean.Elab.Term.Quotation.getPatternVars (stx : Syntax) :
    TermElabM (Array Syntax)

    Get all pattern vars (as Syntax.idents) in stx

    source
    def Lean.Elab.Term.Quotation.getPatternsVars (pats : Array Syntax) :
    TermElabM (Array Syntax)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Term.Quotation.getAntiquotKindSpec? (antiquot : Syntax) :
      Option Syntax

      Given an antiquotation like $e:term (i.e. Syntax.antiquotKind? returns some), returns the "term" atom if present.

      Equations
      Instances For