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

• quotLCtx : Lean.NameSet

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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 : Lake.Name) (x : Lean.Elab.Term.Quotation.PrecheckM α) : Lean.Elab.Term.Quotation.PrecheckM α

Equations

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

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

Equations

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

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

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

unsafe def Lean.Elab.Term.Quotation.mkPrecheckAttribute : IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.Quotation.Precheck)

Equations

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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