structure Lean.Elab.Term.Quotation.Precheck.Context : Type

• quotLCtx : NameSet

@[reducible, inline]

abbrev Lean.Elab.Term.Quotation.PrecheckM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Elab.Term.Quotation.Precheck : Type

def Lean.Elab.Term.Quotation.withNewLocal {α : Type} (l : Name) (x : PrecheckM α) : PrecheckM α

def Lean.Elab.Term.Quotation.withNewLocals {α : Type} (ls : Array Name) (x : PrecheckM α) : PrecheckM α

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

opaque Lean.Elab.Term.Quotation.quotPrecheck.allowSectionVars : Lean.Option Bool

opaque Lean.Elab.Term.Quotation.precheckAttribute : KeyedDeclsAttribute Precheck

Registers a double backtick syntax quotation pre-check.

@[quot_precheck k] registers a declaration of type Lean.Elab.Term.Quotation.Precheck for the syntax node kind k. It should implement eager name analysis on the passed syntax by throwing an exception on unbound identifiers, and calling precheck recursively on nested terms, potentially with an extended local context (withNewLocal). Macros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.

partial def Lean.Elab.Term.Quotation.precheck : Precheck

partial def Lean.Elab.Term.Quotation.precheck.hasQuotedIdent : Syntax → Bool

def Lean.Elab.Term.Quotation.runPrecheck (stx : Syntax) : TermElabM Unit

def Lean.Elab.Term.Quotation.precheckIdent : Precheck

def Lean.Elab.Term.Quotation.precheckApp : Precheck

def Lean.Elab.Term.Quotation.precheckTypeAscription : Precheck

def Lean.Elab.Term.Quotation.precheckExplicit : Precheck

def Lean.Elab.Term.Quotation.precheckChoice : Precheck

def Lean.Elab.Term.Quotation.elabPrecheckedQuot : TermElab

def Lean.Elab.Term.Quotation.precheckBinrel : Precheck

def Lean.Elab.Term.Quotation.precheckBinrelNoProp : Precheck

def Lean.Elab.Term.Quotation.precheckBinop : Precheck

def Lean.Elab.Term.Quotation.precheckBinopLazy : Precheck

def Lean.Elab.Term.Quotation.precheckLeftact : Precheck

def Lean.Elab.Term.Quotation.precheckRightact : Precheck

def Lean.Elab.Term.Quotation.precheckUnop : Precheck