Documentation

Lean.PrettyPrinter.Delaborator.Options

constant Lean.pp.all :

Lean.Option Bool

constant Lean.pp.notation :

Lean.Option Bool

constant Lean.pp.match :

Lean.Option Bool

constant Lean.pp.coercions :

Lean.Option Bool

constant Lean.pp.universes :

Lean.Option Bool

constant Lean.pp.fullNames :

Lean.Option Bool

constant Lean.pp.privateNames :

Lean.Option Bool

constant Lean.pp.funBinderTypes :

Lean.Option Bool

constant Lean.pp.piBinderTypes :

Lean.Option Bool

constant Lean.pp.letVarTypes :

Lean.Option Bool

constant Lean.pp.instantiateMVars :

Lean.Option Bool

constant Lean.pp.structureInstances :

Lean.Option Bool

constant Lean.pp.structureProjections :

Lean.Option Bool

constant Lean.pp.explicit :

Lean.Option Bool

constant Lean.pp.structureInstanceTypes :

Lean.Option Bool

constant Lean.pp.safeShadowing :

Lean.Option Bool

constant Lean.pp.tagAppFns :

Lean.Option Bool

constant Lean.pp.proofs :

Lean.Option Bool

constant Lean.pp.proofs.withType :

Lean.Option Bool

constant Lean.pp.instances :

Lean.Option Bool

constant Lean.pp.instanceTypes :

Lean.Option Bool

constant Lean.pp.motives.pi :

Lean.Option Bool

constant Lean.pp.motives.nonConst :

Lean.Option Bool

constant Lean.pp.motives.all :

Lean.Option Bool

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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