opaque Lean.pp.maxSteps : Lean.Option Nat

opaque Lean.pp.all : Lean.Option Bool

opaque Lean.pp.notation : Lean.Option Bool

opaque Lean.pp.parens : Lean.Option Bool

opaque Lean.pp.unicode.fun : Lean.Option Bool

opaque Lean.pp.match : Lean.Option Bool

opaque Lean.pp.coercions : Lean.Option Bool

opaque Lean.pp.coercions.types : Lean.Option Bool

opaque Lean.pp.universes : Lean.Option Bool

opaque Lean.pp.fullNames : Lean.Option Bool

opaque Lean.pp.privateNames : Lean.Option Bool

opaque Lean.pp.funBinderTypes : Lean.Option Bool

opaque Lean.pp.piBinderTypes : Lean.Option Bool

opaque Lean.pp.letVarTypes : Lean.Option Bool

opaque Lean.pp.natLit : Lean.Option Bool

opaque Lean.pp.numericTypes : Lean.Option Bool

opaque Lean.pp.instantiateMVars : Lean.Option Bool

opaque Lean.pp.mvars : Lean.Option Bool

opaque Lean.pp.mvars.levels : Lean.Option Bool

opaque Lean.pp.mvars.anonymous : Lean.Option Bool

opaque Lean.pp.mvars.withType : Lean.Option Bool

opaque Lean.pp.mvars.delayed : Lean.Option Bool

opaque Lean.pp.beta : Lean.Option Bool

opaque Lean.pp.structureInstances : Lean.Option Bool

opaque Lean.pp.structureInstances.flatten : Lean.Option Bool

opaque Lean.pp.fieldNotation : Lean.Option Bool

opaque Lean.pp.fieldNotation.generalized : Lean.Option Bool

opaque Lean.pp.explicit : Lean.Option Bool

opaque Lean.pp.structureInstanceTypes : Lean.Option Bool

opaque Lean.pp.safeShadowing : Lean.Option Bool

opaque Lean.pp.tagAppFns : Lean.Option Bool

opaque Lean.pp.proofs : Lean.Option Bool

opaque Lean.pp.proofs.withType : Lean.Option Bool

opaque Lean.pp.proofs.threshold : Lean.Option Nat

opaque Lean.pp.instances : Lean.Option Bool

opaque Lean.pp.instanceTypes : Lean.Option Bool

opaque Lean.pp.deepTerms : Lean.Option Bool

opaque Lean.pp.deepTerms.threshold : Lean.Option Nat

opaque Lean.pp.motives.pi : Lean.Option Bool

opaque Lean.pp.motives.nonConst : Lean.Option Bool

opaque Lean.pp.motives.all : Lean.Option Bool

def Lean.getPPMaxSteps (o : Lean.Options) : Nat

def Lean.getPPAll (o : Lean.Options) : Bool

def Lean.getPPFunBinderTypes (o : Lean.Options) : Bool

def Lean.getPPPiBinderTypes (o : Lean.Options) : Bool

def Lean.getPPLetVarTypes (o : Lean.Options) : Bool

def Lean.getPPNumericTypes (o : Lean.Options) : Bool

Equations

• Lean.getPPNumericTypes o = Lean.KVMap.get o Lean.pp.numericTypes.name Lean.pp.numericTypes.defValue

def Lean.getPPNatLit (o : Lean.Options) : Bool

Equations

• Lean.getPPNatLit o = Lean.KVMap.get o Lean.pp.natLit.name (Lean.getPPNumericTypes o && !Lean.getPPAll o)

def Lean.getPPCoercions (o : Lean.Options) : Bool

def Lean.getPPCoercionsTypes (o : Lean.Options) : Bool

def Lean.getPPExplicit (o : Lean.Options) : Bool

Equations

• Lean.getPPExplicit o = Lean.KVMap.get o Lean.pp.explicit.name (Lean.getPPAll o)

def Lean.getPPNotation (o : Lean.Options) : Bool

Equations

• Lean.getPPNotation o = Lean.KVMap.get o Lean.pp.notation.name !Lean.getPPAll o

def Lean.getPPParens (o : Lean.Options) : Bool

Equations

• Lean.getPPParens o = Lean.KVMap.get o Lean.pp.parens.name Lean.pp.parens.defValue

def Lean.getPPUnicodeFun (o : Lean.Options) : Bool

Equations

• Lean.getPPUnicodeFun o = Lean.KVMap.get o Lean.pp.unicode.fun.name false

def Lean.getPPMatch (o : Lean.Options) : Bool

def Lean.getPPFieldNotation (o : Lean.Options) : Bool

Equations

• Lean.getPPFieldNotation o = Lean.KVMap.get o Lean.pp.fieldNotation.name !Lean.getPPAll o

def Lean.getPPFieldNotationGeneralized (o : Lean.Options) : Bool

def Lean.getPPStructureInstances (o : Lean.Options) : Bool

Equations

• Lean.getPPStructureInstances o = Lean.KVMap.get o Lean.pp.structureInstances.name !Lean.getPPAll o

def Lean.getPPStructureInstancesFlatten (o : Lean.Options) : Bool

def Lean.getPPStructureInstanceType (o : Lean.Options) : Bool

def Lean.getPPTagAppFns (o : Lean.Options) : Bool

def Lean.getPPUniverses (o : Lean.Options) : Bool

def Lean.getPPFullNames (o : Lean.Options) : Bool

Equations

• Lean.getPPFullNames o = Lean.KVMap.get o Lean.pp.fullNames.name (Lean.getPPAll o)

def Lean.getPPPrivateNames (o : Lean.Options) : Bool

Equations

• Lean.getPPPrivateNames o = Lean.KVMap.get o Lean.pp.privateNames.name (Lean.getPPAll o)

def Lean.getPPInstantiateMVars (o : Lean.Options) : Bool

Equations

• Lean.getPPInstantiateMVars o = Lean.KVMap.get o Lean.pp.instantiateMVars.name Lean.pp.instantiateMVars.defValue

def Lean.getPPMVars (o : Lean.Options) : Bool

def Lean.getPPMVarsAnonymous (o : Lean.Options) : Bool

Equations

• Lean.getPPMVarsAnonymous o = Lean.KVMap.get o Lean.pp.mvars.anonymous.name (Lean.pp.mvars.anonymous.defValue && Lean.getPPMVars o)

def Lean.getPPMVarsLevels (o : Lean.Options) : Bool

def Lean.getPPMVarsWithType (o : Lean.Options) : Bool

def Lean.getPPMVarsDelayed (o : Lean.Options) : Bool

Equations

• Lean.getPPMVarsDelayed o = Lean.KVMap.get o Lean.pp.mvars.delayed.name (Lean.pp.mvars.delayed.defValue || Lean.getPPAll o)

def Lean.getPPBeta (o : Lean.Options) : Bool

def Lean.getPPSafeShadowing (o : Lean.Options) : Bool

def Lean.getPPProofs (o : Lean.Options) : Bool

def Lean.getPPProofsWithType (o : Lean.Options) : Bool

def Lean.getPPProofsThreshold (o : Lean.Options) : Nat

def Lean.getPPMotivesPi (o : Lean.Options) : Bool

Equations

• Lean.getPPMotivesPi o = Lean.KVMap.get o Lean.pp.motives.pi.name Lean.pp.motives.pi.defValue

def Lean.getPPMotivesNonConst (o : Lean.Options) : Bool

Equations

• Lean.getPPMotivesNonConst o = Lean.KVMap.get o Lean.pp.motives.nonConst.name Lean.pp.motives.nonConst.defValue

def Lean.getPPMotivesAll (o : Lean.Options) : Bool

Equations

• Lean.getPPMotivesAll o = Lean.KVMap.get o Lean.pp.motives.all.name Lean.pp.motives.all.defValue

def Lean.getPPInstances (o : Lean.Options) : Bool

def Lean.getPPInstanceTypes (o : Lean.Options) : Bool

def Lean.getPPDeepTerms (o : Lean.Options) : Bool

def Lean.getPPDeepTermsThreshold (o : Lean.Options) : Nat