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

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

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

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.
• Lean.Elab.Term.Quotation.precheckIdent stx = Lean.Elab.throwUnsupportedSyntax

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.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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