Documentation

Lean.PrettyPrinter.Delaborator.Options

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) :

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For