opaque Lean.pp.all : Lean.Option Bool

opaque Lean.pp.notation : 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.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.beta : Lean.Option Bool

opaque Lean.pp.structureInstances : Lean.Option Bool

opaque Lean.pp.structureProjections : 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.getPPAll (o : Lean.Options) : Bool

Equations

• Lean.getPPAll o = Lean.KVMap.get o Lean.pp.all.name false

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

Equations

• Lean.getPPFunBinderTypes o = Lean.KVMap.get o Lean.pp.funBinderTypes.name (Lean.getPPAll o)

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

Equations

• Lean.getPPPiBinderTypes o = Lean.KVMap.get o Lean.pp.piBinderTypes.name Lean.pp.piBinderTypes.defValue

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

Equations

• Lean.getPPLetVarTypes o = Lean.KVMap.get o Lean.pp.letVarTypes.name (Lean.getPPAll o)

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

Equations

• Lean.getPPCoercions o = Lean.KVMap.get o Lean.pp.coercions.name !Lean.getPPAll o

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.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

Equations

• Lean.getPPMatch o = Lean.KVMap.get o Lean.pp.match.name !Lean.getPPAll o

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

Equations

• Lean.getPPStructureProjections o = Lean.KVMap.get o Lean.pp.structureProjections.name !Lean.getPPAll o

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

Equations

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

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

Equations

• Lean.getPPStructureInstanceType o = Lean.KVMap.get o Lean.pp.structureInstanceTypes.name (Lean.getPPAll o)

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

Equations

• Lean.getPPTagAppFns o = Lean.KVMap.get o Lean.pp.tagAppFns.name (Lean.getPPAll o)

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

Equations

• Lean.getPPUniverses o = Lean.KVMap.get o Lean.pp.universes.name (Lean.getPPAll o)

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.getPPBeta (o : Lean.Options) : Bool

Equations

• Lean.getPPBeta o = Lean.KVMap.get o Lean.pp.beta.name Lean.pp.beta.defValue

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

Equations

• Lean.getPPSafeShadowing o = Lean.KVMap.get o Lean.pp.safeShadowing.name Lean.pp.safeShadowing.defValue

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

Equations

• Lean.getPPProofs o = Lean.KVMap.get o Lean.pp.proofs.name (Lean.pp.proofs.defValue || Lean.getPPAll o)

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

Equations

• Lean.getPPProofsWithType o = Lean.KVMap.get o Lean.pp.proofs.withType.name Lean.pp.proofs.withType.defValue

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

Equations

• Lean.getPPProofsThreshold o = Lean.KVMap.get o Lean.pp.proofs.threshold.name Lean.pp.proofs.threshold.defValue

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

Equations

• Lean.getPPInstances o = Lean.KVMap.get o Lean.pp.instances.name Lean.pp.instances.defValue

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

Equations

• Lean.getPPInstanceTypes o = Lean.KVMap.get o Lean.pp.instanceTypes.name Lean.pp.instanceTypes.defValue

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

Equations

• Lean.getPPDeepTerms o = Lean.KVMap.get o Lean.pp.deepTerms.name (Lean.pp.deepTerms.defValue || Lean.getPPAll o)

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

Equations

• Lean.getPPDeepTermsThreshold o = Lean.KVMap.get o Lean.pp.deepTerms.threshold.name Lean.pp.deepTerms.threshold.defValue