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.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.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.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
Equations
    Instances For
      source
      def Lean.getPPAll (o : Options) :
      Bool
      Equations
        Instances For
          source
          def Lean.getPPFunBinderTypes (o : Options) :
          Bool
          Equations
            Instances For
              source
              def Lean.getPPPiBinderTypes (o : Options) :
              Bool
              Equations
                Instances For
                  source
                  def Lean.getPPLetVarTypes (o : Options) :
                  Bool
                  Equations
                    Instances For
                      source
                      def Lean.getPPNumericTypes (o : Options) :
                      Bool
                      Equations
                        Instances For
                          source
                          def Lean.getPPNatLit (o : Options) :
                          Bool
                          Equations
                            Instances For
                              source
                              def Lean.getPPCoercions (o : Options) :
                              Bool
                              Equations
                                Instances For
                                  source
                                  def Lean.getPPCoercionsTypes (o : Options) :
                                  Bool
                                  Equations
                                    Instances For
                                      source
                                      def Lean.getPPExplicit (o : Options) :
                                      Bool
                                      Equations
                                        Instances For
                                          source
                                          def Lean.getPPForalls (o : Options) :
                                          Bool
                                          Equations
                                            Instances For
                                              source
                                              def Lean.getPPNotation (o : Options) :
                                              Bool
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.getPPParens (o : Options) :
                                                  Bool
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.getPPUnicodeFun (o : Options) :
                                                      Bool
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.getPPMatch (o : Options) :
                                                          Bool
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.getPPSorrySource (o : Options) :
                                                              Bool
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.getPPFieldNotation (o : Options) :
                                                                  Bool
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.getPPFieldNotationGeneralized (o : Options) :
                                                                      Bool
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.getPPStructureInstances (o : Options) :
                                                                          Bool
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lean.getPPStructureInstancesFlatten (o : Options) :
                                                                              Bool
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.getPPStructureInstancesDefaults (o : Options) :
                                                                                  Bool
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.getPPStructureInstanceType (o : Options) :
                                                                                      Bool
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.getPPTagAppFns (o : Options) :
                                                                                          Bool
                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.getPPUniverses (o : Options) :
                                                                                              Bool
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lean.getPPFullNames (o : Options) :
                                                                                                  Bool
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lean.getPPPrivateNames (o : Options) :
                                                                                                      Bool
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lean.getPPInstantiateMVars (o : Options) :
                                                                                                          Bool
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.getPPMVars (o : Options) :
                                                                                                              Bool
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.getPPMVarsAnonymous (o : Options) :
                                                                                                                  Bool
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lean.getPPMVarsLevels (o : Options) :
                                                                                                                      Bool
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lean.getPPMVarsWithType (o : Options) :
                                                                                                                          Bool
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Lean.getPPMVarsDelayed (o : Options) :
                                                                                                                              Bool
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def Lean.getPPBeta (o : Options) :
                                                                                                                                  Bool
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def Lean.getPPSafeShadowing (o : Options) :
                                                                                                                                      Bool
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def Lean.getPPProofs (o : Options) :
                                                                                                                                          Bool
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              def Lean.getPPProofsWithType (o : Options) :
                                                                                                                                              Bool
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  source
                                                                                                                                                  def Lean.getPPProofsThreshold (o : Options) :
                                                                                                                                                  Nat
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      source
                                                                                                                                                      def Lean.getPPMotivesPi (o : Options) :
                                                                                                                                                      Bool
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          source
                                                                                                                                                          def Lean.getPPMotivesNonConst (o : Options) :
                                                                                                                                                          Bool
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              source
                                                                                                                                                              def Lean.getPPMotivesAll (o : Options) :
                                                                                                                                                              Bool
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  source
                                                                                                                                                                  def Lean.getPPInstances (o : Options) :
                                                                                                                                                                  Bool
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      source
                                                                                                                                                                      def Lean.getPPInstanceTypes (o : Options) :
                                                                                                                                                                      Bool
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          source
                                                                                                                                                                          def Lean.getPPDeepTerms (o : Options) :
                                                                                                                                                                          Bool
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              source
                                                                                                                                                                              def Lean.getPPDeepTermsThreshold (o : Options) :
                                                                                                                                                                              Nat
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For