Documentation

Lean.PrettyPrinter.Delaborator.Options

source
opaque Lean.pp.maxSteps :
Lean.Option Nat
source
opaque Lean.pp.all :
Lean.Option Bool
source
opaque Lean.pp.notation :
Lean.Option Bool
source
opaque Lean.pp.parens :
Lean.Option Bool
source
opaque Lean.pp.unicode :
Lean.Option Bool
source
opaque Lean.pp.unicode.fun :
Lean.Option Bool
source
opaque Lean.pp.match :
Lean.Option Bool
source
opaque Lean.pp.sorrySource :
Lean.Option Bool
source
opaque Lean.pp.coercions :
Lean.Option Bool
source
opaque Lean.pp.coercions.types :
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.piBinderNames :
Lean.Option Bool
source
opaque Lean.pp.piBinderNames.hygienic :
Lean.Option Bool
source
opaque Lean.pp.foralls :
Lean.Option Bool
source
opaque Lean.pp.letVarTypes :
Lean.Option Bool
source
opaque Lean.pp.natLit :
Lean.Option Bool
source
opaque Lean.pp.numericTypes :
Lean.Option Bool
source
opaque Lean.pp.instantiateMVars :
Lean.Option Bool
source
opaque Lean.pp.mvars :
Lean.Option Bool
source
opaque Lean.pp.mvars.levels :
Lean.Option Bool
source
opaque Lean.pp.mvars.anonymous :
Lean.Option Bool
source
opaque Lean.pp.mvars.withType :
Lean.Option Bool
source
opaque Lean.pp.mvars.delayed :
Lean.Option Bool
source
opaque Lean.pp.fvars.anonymous :
Lean.Option Bool
source
opaque Lean.pp.beta :
Lean.Option Bool
source
opaque Lean.pp.structureInstances :
Lean.Option Bool
source
opaque Lean.pp.structureInstances.flatten :
Lean.Option Bool
source
opaque Lean.pp.structureInstances.defaults :
Lean.Option Bool
source
opaque Lean.pp.fieldNotation :
Lean.Option Bool
source
opaque Lean.pp.fieldNotation.generalized :
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.proofs.threshold :
Lean.Option Nat
source
opaque Lean.pp.instances :
Lean.Option Bool
source
opaque Lean.pp.instanceTypes :
Lean.Option Bool
source
opaque Lean.pp.deepTerms :
Lean.Option Bool
source
opaque Lean.pp.deepTerms.threshold :
Lean.Option Nat
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.getPPMaxSteps (o : Options) :
Nat
Instances For
    source
    def Lean.getPPAll (o : Options) :
    Bool
    Instances For
      source
      def Lean.getPPFunBinderTypes (o : Options) :
      Bool
      Instances For
        source
        def Lean.getPPPiBinderTypes (o : Options) :
        Bool
        Instances For
          source
          def Lean.getPPPiBinderNames (o : Options) :
          Bool
          Instances For
            source
            def Lean.getPPPiBinderNamesHygienic (o : Options) :
            Bool
            Instances For
              source
              def Lean.getPPLetVarTypes (o : Options) :
              Bool
              Instances For
                source
                def Lean.getPPNumericTypes (o : Options) :
                Bool
                Instances For
                  source
                  def Lean.getPPNatLit (o : Options) :
                  Bool
                  Instances For
                    source
                    def Lean.getPPCoercions (o : Options) :
                    Bool
                    Instances For
                      source
                      def Lean.getPPCoercionsTypes (o : Options) :
                      Bool
                      Instances For
                        source
                        def Lean.getPPExplicit (o : Options) :
                        Bool
                        Instances For
                          source
                          def Lean.getPPForalls (o : Options) :
                          Bool
                          Instances For
                            source
                            def Lean.getPPNotation (o : Options) :
                            Bool
                            Instances For
                              source
                              def Lean.getPPParens (o : Options) :
                              Bool
                              Instances For
                                source
                                def Lean.getPPUnicode (o : Options) :
                                Bool
                                Instances For
                                  source
                                  def Lean.getPPUnicodeFun (o : Options) :
                                  Bool
                                  Instances For
                                    source
                                    def Lean.getPPMatch (o : Options) :
                                    Bool
                                    Instances For
                                      source
                                      def Lean.getPPSorrySource (o : Options) :
                                      Bool
                                      Instances For
                                        source
                                        def Lean.getPPFieldNotation (o : Options) :
                                        Bool
                                        Instances For
                                          source
                                          def Lean.getPPFieldNotationGeneralized (o : Options) :
                                          Bool
                                          Instances For
                                            source
                                            def Lean.getPPStructureInstances (o : Options) :
                                            Bool
                                            Instances For
                                              source
                                              def Lean.getPPStructureInstancesFlatten (o : Options) :
                                              Bool
                                              Instances For
                                                source
                                                def Lean.getPPStructureInstancesDefaults (o : Options) :
                                                Bool
                                                Instances For
                                                  source
                                                  def Lean.getPPStructureInstanceType (o : Options) :
                                                  Bool
                                                  Instances For
                                                    source
                                                    def Lean.getPPTagAppFns (o : Options) :
                                                    Bool
                                                    Instances For
                                                      source
                                                      def Lean.getPPUniverses (o : Options) :
                                                      Bool
                                                      Instances For
                                                        source
                                                        def Lean.getPPFullNames (o : Options) :
                                                        Bool
                                                        Instances For
                                                          source
                                                          def Lean.getPPPrivateNames (o : Options) :
                                                          Bool
                                                          Instances For
                                                            source
                                                            def Lean.getPPInstantiateMVars (o : Options) :
                                                            Bool
                                                            Instances For
                                                              source
                                                              def Lean.getPPMVars (o : Options) :
                                                              Bool
                                                              Instances For
                                                                source
                                                                def Lean.getPPMVarsAnonymous (o : Options) :
                                                                Bool
                                                                Instances For
                                                                  source
                                                                  def Lean.getPPMVarsLevels (o : Options) :
                                                                  Bool
                                                                  Instances For
                                                                    source
                                                                    def Lean.getPPMVarsWithType (o : Options) :
                                                                    Bool
                                                                    Instances For
                                                                      source
                                                                      def Lean.getPPMVarsDelayed (o : Options) :
                                                                      Bool
                                                                      Instances For
                                                                        source
                                                                        def Lean.getPPFVarsAnonymous (o : Options) :
                                                                        Bool
                                                                        Instances For
                                                                          source
                                                                          def Lean.getPPBeta (o : Options) :
                                                                          Bool
                                                                          Instances For
                                                                            source
                                                                            def Lean.getPPSafeShadowing (o : Options) :
                                                                            Bool
                                                                            Instances For
                                                                              source
                                                                              def Lean.getPPProofs (o : Options) :
                                                                              Bool
                                                                              Instances For
                                                                                source
                                                                                def Lean.getPPProofsWithType (o : Options) :
                                                                                Bool
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.getPPProofsThreshold (o : Options) :
                                                                                  Nat
                                                                                  Instances For
                                                                                    source
                                                                                    def Lean.getPPMotivesPi (o : Options) :
                                                                                    Bool
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.getPPMotivesNonConst (o : Options) :
                                                                                      Bool
                                                                                      Instances For
                                                                                        source
                                                                                        def Lean.getPPMotivesAll (o : Options) :
                                                                                        Bool
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.getPPInstances (o : Options) :
                                                                                          Bool
                                                                                          Instances For
                                                                                            source
                                                                                            def Lean.getPPInstanceTypes (o : Options) :
                                                                                            Bool
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.getPPDeepTerms (o : Options) :
                                                                                              Bool
                                                                                              Instances For
                                                                                                source
                                                                                                def Lean.getPPDeepTermsThreshold (o : Options) :
                                                                                                Nat
                                                                                                Instances For