Documentation

Lean.Elab.Quotation.Util

constant Lean.Elab.Term.Quotation.hygiene :

Lean.Option Bool

def Lean.Elab.Term.Quotation.getAntiquotationIds (stx : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Term.Quotation.getAntiquotationIds stx = let ids := #[]; do let r ← let col := Lean.Syntax.topDown stx; forIn col ids fun stx r => let ids := r; if ((Lean.Syntax.isAntiquot stx || Lean.Syntax.isTokenAntiquot stx) && !Lean.Syntax.isEscapedAntiquot stx) = true then let anti := Lean.Syntax.getAntiquotTerm stx; if Lean.Syntax.isIdent anti = true then let ids := Array.push ids anti; do pure PUnit.unit pure (ForInStep.yield ids) else do Lean.throwErrorAt stx (Lean.toMessageData "complex antiquotation not allowed here") pure (ForInStep.yield ids) else do pure PUnit.unit pure (ForInStep.yield ids) let x : Array Lean.Syntax := r let ids : Array Lean.Syntax := x pure ids

partial def Lean.Elab.Term.Quotation.getPatternVars (stx : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Syntax)

def Lean.Elab.Term.Quotation.getPatternsVars (pats : Array Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Term.Quotation.getPatternsVars pats = Array.foldlM (fun vars pat => do let a ← Lean.Elab.Term.Quotation.getPatternVars pat pure (vars ++ a)) #[] pats 0 (Array.size pats)