Documentation

Lean.PrettyPrinter.Delaborator.Options

source
opaque Lean.pp.all :
Lean.Option Bool
source
opaque Lean.pp.notation :
Lean.Option Bool
source
opaque Lean.pp.unicode.fun :
Lean.Option Bool
source
opaque Lean.pp.match :
Lean.Option Bool
source
opaque Lean.pp.coercions :
Lean.Option Bool
source
opaque Lean.pp.universes :
Lean.Option Bool
source
opaque Lean.pp.fullNames :
Lean.Option Bool
source
opaque Lean.pp.privateNames :
Lean.Option Bool
source
opaque Lean.pp.funBinderTypes :
Lean.Option Bool
source
opaque Lean.pp.piBinderTypes :
Lean.Option Bool
source
opaque Lean.pp.letVarTypes :
Lean.Option Bool
source
opaque Lean.pp.instantiateMVars :
Lean.Option Bool
source
opaque Lean.pp.structureInstances :
Lean.Option Bool
source
opaque Lean.pp.structureProjections :
Lean.Option Bool
source
opaque Lean.pp.explicit :
Lean.Option Bool
source
opaque Lean.pp.structureInstanceTypes :
Lean.Option Bool
source
opaque Lean.pp.safeShadowing :
Lean.Option Bool
source
opaque Lean.pp.tagAppFns :
Lean.Option Bool
source
opaque Lean.pp.proofs :
Lean.Option Bool
source
opaque Lean.pp.proofs.withType :
Lean.Option Bool
source
opaque Lean.pp.instances :
Lean.Option Bool
source
opaque Lean.pp.instanceTypes :
Lean.Option Bool
source
opaque Lean.pp.motives.pi :
Lean.Option Bool
source
opaque Lean.pp.motives.nonConst :
Lean.Option Bool
source
opaque Lean.pp.motives.all :
Lean.Option Bool
source
def Lean.getPPAll (o : Lean.Options) :
Bool
Instances For
    source
    def Lean.getPPFunBinderTypes (o : Lean.Options) :
    Bool
    Instances For
      source
      def Lean.getPPPiBinderTypes (o : Lean.Options) :
      Bool
      Instances For
        source
        def Lean.getPPLetVarTypes (o : Lean.Options) :
        Bool
        Instances For
          source
          def Lean.getPPCoercions (o : Lean.Options) :
          Bool
          Instances For
            source
            def Lean.getPPExplicit (o : Lean.Options) :
            Bool
            Instances For
              source
              def Lean.getPPNotation (o : Lean.Options) :
              Bool
              Instances For
                source
                def Lean.getPPUnicodeFun (o : Lean.Options) :
                Bool
                Instances For
                  source
                  def Lean.getPPMatch (o : Lean.Options) :
                  Bool
                  Instances For
                    source
                    def Lean.getPPStructureProjections (o : Lean.Options) :
                    Bool
                    Instances For
                      source
                      def Lean.getPPStructureInstances (o : Lean.Options) :
                      Bool
                      Instances For
                        source
                        def Lean.getPPStructureInstanceType (o : Lean.Options) :
                        Bool
                        Instances For
                          source
                          def Lean.getPPTagAppFns (o : Lean.Options) :
                          Bool
                          Instances For
                            source
                            def Lean.getPPUniverses (o : Lean.Options) :
                            Bool
                            Instances For
                              source
                              def Lean.getPPFullNames (o : Lean.Options) :
                              Bool
                              Instances For
                                source
                                def Lean.getPPPrivateNames (o : Lean.Options) :
                                Bool
                                Instances For
                                  source
                                  def Lean.getPPInstantiateMVars (o : Lean.Options) :
                                  Bool
                                  Instances For
                                    source
                                    def Lean.getPPSafeShadowing (o : Lean.Options) :
                                    Bool
                                    Instances For
                                      source
                                      def Lean.getPPProofs (o : Lean.Options) :
                                      Bool
                                      Instances For
                                        source
                                        def Lean.getPPProofsWithType (o : Lean.Options) :
                                        Bool
                                        Instances For
                                          source
                                          def Lean.getPPMotivesPi (o : Lean.Options) :
                                          Bool
                                          Instances For
                                            source
                                            def Lean.getPPMotivesNonConst (o : Lean.Options) :
                                            Bool
                                            Instances For
                                              source
                                              def Lean.getPPMotivesAll (o : Lean.Options) :
                                              Bool
                                              Instances For
                                                source
                                                def Lean.getPPInstances (o : Lean.Options) :
                                                Bool
                                                Instances For
                                                  source
                                                  def Lean.getPPInstanceTypes (o : Lean.Options) :
                                                  Bool
                                                  Instances For