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

• quotLCtx : NameSet

@[reducible, inline]

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

Equations

• Lean.Elab.Term.Quotation.PrecheckM = ReaderT Lean.Elab.Term.Quotation.Precheck.Context Lean.Elab.TermElabM

@[reducible, inline]

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

Equations

• Lean.Elab.Term.Quotation.Precheck = (Lean.Syntax → Lean.Elab.Term.Quotation.PrecheckM Unit)

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

Equations

• Lean.Elab.Term.Quotation.withNewLocal l x = withReader (fun (ctx : Lean.Elab.Term.Quotation.Precheck.Context) => { quotLCtx := ctx.quotLCtx.insert l }) x

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

Equations

• Lean.Elab.Term.Quotation.withNewLocals ls x = withReader (fun (ctx : Lean.Elab.Term.Quotation.Precheck.Context) => { quotLCtx := Array.foldl Lean.NameSet.insert ctx.quotLCtx ls }) x

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.Quotation.precheckIdent stx = Lean.Elab.throwUnsupportedSyntax

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.