HepLean 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)
Equations
  • One or more equations did not get rendered due to their size.
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)
    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For