Documentation

Lean.Elab.Quotation.Util

source
opaque Lean.Elab.Term.Quotation.hygiene :
Lean.Option Bool
source
def Lean.Elab.Term.Quotation.getAntiquotationIds (stx : Lean.Syntax) :
Lean.Elab.TermElabM (Array Lean.Ident)
Instances For
    source
    partial def Lean.Elab.Term.Quotation.getPatternVars (stx : Lean.Syntax) :
    Lean.Elab.TermElabM (Array Lean.Syntax)

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

    source
    def Lean.Elab.Term.Quotation.getPatternsVars (pats : Array Lean.Syntax) :
    Lean.Elab.TermElabM (Array Lean.Syntax)
    Instances For
      source
      def Lean.Elab.Term.Quotation.getAntiquotKindSpec? (antiquot : Lean.Syntax) :
      Option Lean.Syntax

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

      Instances For