Documentation
Qq
.
Delab
Search
Google site search
Qq
.
Delab
source
Imports
Init
Qq.Macro
Imported by
Qq
.
Impl
.
pp
.
qq
Qq
.
Impl
.
checkQqDelabOptions
Qq
.
Impl
.
instMonadLiftUnquoteMStateTUnquoteStateDelabM
Qq
.
Impl
.
delabQuoted
Qq
.
Impl
.
withDelabQuoted
Qq
.
Impl
.
delabQuotedLevel
Qq
.
Impl
.
delabQ
Qq
.
Impl
.
delabq
Qq
.
Impl
.
delabQuotedDefEq
Qq
.
Impl
.
delabQuotedLevelDefEq
source
opaque
Qq
.
Impl
.
pp
.
qq
:
Lean.Option
Bool
source
def
Qq
.
Impl
.
checkQqDelabOptions
:
Lean.PrettyPrinter.Delaborator.DelabM
Unit
Instances For
source
instance
Qq
.
Impl
.
instMonadLiftUnquoteMStateTUnquoteStateDelabM
:
MonadLift
Qq.Impl.UnquoteM
(
StateT
Qq.Impl.UnquoteState
Lean.PrettyPrinter.Delaborator.DelabM
)
source
def
Qq
.
Impl
.
delabQuoted
:
StateT
Qq.Impl.UnquoteState
Lean.PrettyPrinter.Delaborator.DelabM
Lean.Term
Instances For
source
def
Qq
.
Impl
.
withDelabQuoted
(k :
StateT
Qq.Impl.UnquoteState
Lean.PrettyPrinter.Delaborator.DelabM
Lean.Term
)
:
Lean.PrettyPrinter.Delaborator.Delab
Instances For
source
def
Qq
.
Impl
.
delabQuotedLevel
:
Lean.PrettyPrinter.Delaborator.DelabM
Lean.Syntax.Level
Instances For
source
def
Qq
.
Impl
.
delabQ
:
Lean.PrettyPrinter.Delaborator.Delab
Instances For
source
def
Qq
.
Impl
.
delabq
:
Lean.PrettyPrinter.Delaborator.Delab
Instances For
source
def
Qq
.
Impl
.
delabQuotedDefEq
:
Lean.PrettyPrinter.Delaborator.Delab
Instances For
source
def
Qq
.
Impl
.
delabQuotedLevelDefEq
:
Lean.PrettyPrinter.Delaborator.Delab
Instances For