Documentation
Lean
.
PrettyPrinter
.
Delaborator
.
Options
Search
Google site search
Lean
.
PrettyPrinter
.
Delaborator
.
Options
source
Imports
Init
Lean.Data.Options
Imported by
Lean
.
pp
.
all
Lean
.
pp
.
notation
Lean
.
pp
.
unicode
.
fun
Lean
.
pp
.
match
Lean
.
pp
.
coercions
Lean
.
pp
.
universes
Lean
.
pp
.
fullNames
Lean
.
pp
.
privateNames
Lean
.
pp
.
funBinderTypes
Lean
.
pp
.
piBinderTypes
Lean
.
pp
.
letVarTypes
Lean
.
pp
.
instantiateMVars
Lean
.
pp
.
structureInstances
Lean
.
pp
.
structureProjections
Lean
.
pp
.
explicit
Lean
.
pp
.
structureInstanceTypes
Lean
.
pp
.
safeShadowing
Lean
.
pp
.
tagAppFns
Lean
.
pp
.
proofs
Lean
.
pp
.
proofs
.
withType
Lean
.
pp
.
instances
Lean
.
pp
.
instanceTypes
Lean
.
pp
.
motives
.
pi
Lean
.
pp
.
motives
.
nonConst
Lean
.
pp
.
motives
.
all
Lean
.
getPPAll
Lean
.
getPPFunBinderTypes
Lean
.
getPPPiBinderTypes
Lean
.
getPPLetVarTypes
Lean
.
getPPCoercions
Lean
.
getPPExplicit
Lean
.
getPPNotation
Lean
.
getPPUnicodeFun
Lean
.
getPPMatch
Lean
.
getPPStructureProjections
Lean
.
getPPStructureInstances
Lean
.
getPPStructureInstanceType
Lean
.
getPPTagAppFns
Lean
.
getPPUniverses
Lean
.
getPPFullNames
Lean
.
getPPPrivateNames
Lean
.
getPPInstantiateMVars
Lean
.
getPPSafeShadowing
Lean
.
getPPProofs
Lean
.
getPPProofsWithType
Lean
.
getPPMotivesPi
Lean
.
getPPMotivesNonConst
Lean
.
getPPMotivesAll
Lean
.
getPPInstances
Lean
.
getPPInstanceTypes
source
opaque
Lean
.
pp
.
all
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
notation
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
unicode
.
fun
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
match
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
coercions
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
universes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
fullNames
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
privateNames
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
funBinderTypes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
piBinderTypes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
letVarTypes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
instantiateMVars
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
structureInstances
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
structureProjections
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
explicit
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
structureInstanceTypes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
safeShadowing
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
tagAppFns
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
proofs
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
proofs
.
withType
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
instances
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
instanceTypes
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
motives
.
pi
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
motives
.
nonConst
:
Lean.Option
Bool
source
opaque
Lean
.
pp
.
motives
.
all
:
Lean.Option
Bool
source
def
Lean
.
getPPAll
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPFunBinderTypes
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPPiBinderTypes
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPLetVarTypes
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPCoercions
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPExplicit
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPNotation
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPUnicodeFun
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPMatch
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPStructureProjections
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPStructureInstances
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPStructureInstanceType
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPTagAppFns
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPUniverses
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPFullNames
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPPrivateNames
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPInstantiateMVars
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPSafeShadowing
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPProofs
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPProofsWithType
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPMotivesPi
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPMotivesNonConst
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPMotivesAll
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPInstances
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
getPPInstanceTypes
(o :
Lean.Options
)
:
Bool
Instances For