← Mathematical handbook

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 : Lean.Option Bool

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

opaque Lean.pp.match : Lean.Option Bool

opaque Lean.pp.sorrySource : 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.piBinderNames : Lean.Option Bool

opaque Lean.pp.piBinderNames.hygienic : Lean.Option Bool

opaque Lean.pp.foralls : 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.mdata : 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.fvars.anonymous : 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.structureInstances.defaults : 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 : Options) : Nat

Equations

• Lean.getPPMaxSteps o = o.get Lean.pp.maxSteps.name Lean.pp.maxSteps.defValue

def Lean.getPPAll (o : Options) : Bool

Equations

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

def Lean.getPPFunBinderTypes (o : Options) : Bool

Equations

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

def Lean.getPPPiBinderTypes (o : Options) : Bool

Equations

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

def Lean.getPPPiBinderNames (o : Options) : Bool

Equations

• Lean.getPPPiBinderNames o = o.get Lean.pp.piBinderNames.name (Lean.getPPAll o)

def Lean.getPPPiBinderNamesHygienic (o : Options) : Bool

Equations

• Lean.getPPPiBinderNamesHygienic o = o.get Lean.pp.piBinderNames.hygienic.name Lean.pp.piBinderNames.hygienic.defValue

def Lean.getPPLetVarTypes (o : Options) : Bool

Equations

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

def Lean.getPPNumericTypes (o : Options) : Bool

Equations

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

def Lean.getPPNatLit (o : Options) : Bool

Equations

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

def Lean.getPPCoercions (o : Options) : Bool

Equations

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

def Lean.getPPCoercionsTypes (o : Options) : Bool

Equations

• Lean.getPPCoercionsTypes o = o.get Lean.pp.coercions.types.name Lean.pp.coercions.types.defValue

def Lean.getPPExplicit (o : Options) : Bool

Equations

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

def Lean.getPPForalls (o : Options) : Bool

Equations

• Lean.getPPForalls o = o.get Lean.pp.foralls.name Lean.pp.foralls.defValue

def Lean.getPPNotation (o : Options) : Bool

Equations

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

def Lean.getPPParens (o : Options) : Bool

Equations

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

def Lean.getPPUnicode (o : Options) : Bool

Equations

• Lean.getPPUnicode o = o.get Lean.pp.unicode.name Lean.pp.unicode.defValue

def Lean.getPPUnicodeFun (o : Options) : Bool

Equations

• Lean.getPPUnicodeFun o = o.get Lean.pp.unicode.fun.name Lean.pp.unicode.fun.defValue

def Lean.getPPMatch (o : Options) : Bool

Equations

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

def Lean.getPPSorrySource (o : Options) : Bool

Equations

• Lean.getPPSorrySource o = o.get Lean.pp.sorrySource.name Lean.pp.sorrySource.defValue

def Lean.getPPFieldNotation (o : Options) : Bool

Equations

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

def Lean.getPPFieldNotationGeneralized (o : Options) : Bool

Equations

• Lean.getPPFieldNotationGeneralized o = o.get Lean.pp.fieldNotation.generalized.name Lean.pp.fieldNotation.generalized.defValue

def Lean.getPPStructureInstances (o : Options) : Bool

Equations

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

def Lean.getPPStructureInstancesFlatten (o : Options) : Bool

Equations

• Lean.getPPStructureInstancesFlatten o = o.get Lean.pp.structureInstances.flatten.name Lean.pp.structureInstances.flatten.defValue

def Lean.getPPStructureInstancesDefaults (o : Options) : Bool

Equations

• Lean.getPPStructureInstancesDefaults o = o.get Lean.pp.structureInstances.defaults.name Lean.pp.structureInstances.defaults.defValue

def Lean.getPPStructureInstanceType (o : Options) : Bool

Equations

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

def Lean.getPPTagAppFns (o : Options) : Bool

Equations

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

def Lean.getPPUniverses (o : Options) : Bool

Equations

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

def Lean.getPPFullNames (o : Options) : Bool

Equations

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

def Lean.getPPPrivateNames (o : Options) : Bool

Equations

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

def Lean.getPPMData (o : Options) : Bool

Equations

• Lean.getPPMData o = o.get Lean.pp.mdata.name Lean.pp.mdata.defValue

def Lean.getPPInstantiateMVars (o : Options) : Bool

Equations

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

def Lean.getPPMVars (o : Options) : Bool

Equations

• Lean.getPPMVars o = o.get Lean.pp.mvars.name Lean.pp.mvars.defValue

def Lean.getPPMVarsAnonymous (o : Options) : Bool

Equations

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

def Lean.getPPMVarsLevels (o : Options) : Bool

Equations

• Lean.getPPMVarsLevels o = o.get Lean.pp.mvars.levels.name (Lean.pp.mvars.levels.defValue && Lean.getPPMVarsAnonymous o)

def Lean.getPPMVarsWithType (o : Options) : Bool

Equations

• Lean.getPPMVarsWithType o = o.get Lean.pp.mvars.withType.name Lean.pp.mvars.withType.defValue

def Lean.getPPMVarsDelayed (o : Options) : Bool

Equations

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

def Lean.getPPFVarsAnonymous (o : Options) : Bool

Equations

• Lean.getPPFVarsAnonymous o = o.get Lean.pp.fvars.anonymous.name Lean.pp.fvars.anonymous.defValue

def Lean.getPPBeta (o : Options) : Bool

Equations

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

def Lean.getPPSafeShadowing (o : Options) : Bool

Equations

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

def Lean.getPPProofs (o : Options) : Bool

Equations

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

def Lean.getPPProofsWithType (o : Options) : Bool

Equations

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

def Lean.getPPProofsThreshold (o : Options) : Nat

Equations

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

def Lean.getPPMotivesPi (o : Options) : Bool

Equations

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

def Lean.getPPMotivesNonConst (o : Options) : Bool

Equations

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

def Lean.getPPMotivesAll (o : Options) : Bool

Equations

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

def Lean.getPPInstances (o : Options) : Bool

Equations

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

def Lean.getPPInstanceTypes (o : Options) : Bool

Equations

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

def Lean.getPPDeepTerms (o : Options) : Bool

Equations

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

def Lean.getPPDeepTermsThreshold (o : Options) : Nat

Equations

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