Delaborators for q() and Q() notation

opaque Qq.Impl.pp.qq : Lean.Option Bool

def Qq.Impl.checkQqDelabOptions : Lean.PrettyPrinter.Delaborator.DelabM Unit

Equations

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

instance Qq.Impl.instMonadLiftUnquoteMStateTUnquoteStateDelabM : MonadLift Qq.Impl.UnquoteM (StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM)

Equations

• Qq.Impl.instMonadLiftUnquoteMStateTUnquoteStateDelabM = { monadLift := fun {α : Type} (k : Qq.Impl.UnquoteM α) (s : Qq.Impl.UnquoteState) => liftM (k s) }

def Qq.Impl.delabQuoted : StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

Equations

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

def Qq.Impl.withDelabQuoted (k : StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Qq.Impl.delabQuotedLevel : Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax.Level

Equations

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

def Qq.Impl.delabQ : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Qq.Impl.delabq : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Qq.Impl.delabQuotedDefEq : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Qq.Impl.delabQuotedLevelDefEq : Lean.PrettyPrinter.Delaborator.Delab

Equations

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