opaque Lean.Elab.Term.Quotation.hygiene : Lean.Option Bool

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.

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

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.

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

• Lean.Elab.Term.Quotation.getAntiquotKindSpec? antiquot = let name := antiquot[3][1]; if Lean.Syntax.isMissing name = true then none else some name