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

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

Equations

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

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

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.