Documentation

Lean.Elab.Quotation.Precheck

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

Type

quotLCtx : Lean.NameSet

@[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

@[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 => { quotLCtx := Lean.NameSet.insert ctx.quotLCtx 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 => { 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.precheckParen:

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.