Documentation

Mathlib.Data.FP.Basic

Implementation of floating-point numbers (experimental). #

def Int.shift2 (a : ) (b : ) :
Equations
Instances For
    inductive FP.RMode :
    Instances For
      • prec :
      • emax :
      • precPos : 0 < FP.FloatCfg.prec
      • precMax : FP.FloatCfg.prec FP.FloatCfg.emax
      Instances
        theorem FP.FloatCfg.precPos [self : FP.FloatCfg] :
        0 < FP.FloatCfg.prec
        theorem FP.FloatCfg.precMax [self : FP.FloatCfg] :
        FP.FloatCfg.prec FP.FloatCfg.emax
        Equations
        • FP.prec = FP.FloatCfg.prec
        Instances For
          Equations
          • FP.emax = FP.FloatCfg.emax
          Instances For
            Equations
            • FP.emin = 1 - FP.FloatCfg.emax
            Instances For
              def FP.ValidFinite [C : FP.FloatCfg] (e : ) (m : ) :
              Equations
              Instances For
                instance FP.decValidFinite [C : FP.FloatCfg] (e : ) (m : ) :
                Equations
                inductive FP.Float [C : FP.FloatCfg] :
                Instances For
                  def FP.Float.isFinite [C : FP.FloatCfg] :
                  FP.FloatBool
                  Equations
                  Instances For
                    def FP.toRat [C : FP.FloatCfg] (f : FP.Float) :
                    f.isFinite = true
                    Equations
                    Instances For
                      def FP.Float.zero [C : FP.FloatCfg] (s : Bool) :
                      FP.Float
                      Equations
                      Instances For
                        Equations
                        def FP.Float.sign' [C : FP.FloatCfg] :
                        FP.FloatSemiquot Bool
                        Equations
                        Instances For
                          def FP.Float.sign [C : FP.FloatCfg] :
                          FP.FloatBool
                          Equations
                          Instances For
                            def FP.Float.isZero [C : FP.FloatCfg] :
                            FP.FloatBool
                            Equations
                            Instances For
                              def FP.Float.neg [C : FP.FloatCfg] :
                              FP.FloatFP.Float
                              Equations
                              Instances For
                                def FP.divNatLtTwoPow (n : ) (d : ) :
                                Bool
                                Equations
                                Instances For
                                  unsafe def FP.ofPosRatDn [C : FP.FloatCfg] (n : ℕ+) (d : ℕ+) :
                                  FP.Float × Bool
                                  Instances For
                                    unsafe def FP.nextUpPos [C : FP.FloatCfg] (e : ) (m : ) (v : FP.ValidFinite e m) :
                                    FP.Float
                                    Instances For
                                      unsafe def FP.nextDnPos [C : FP.FloatCfg] (e : ) (m : ) (v : FP.ValidFinite e m) :
                                      FP.Float
                                      Instances For
                                        unsafe def FP.nextUp [C : FP.FloatCfg] :
                                        FP.FloatFP.Float
                                        Instances For
                                          unsafe def FP.nextDn [C : FP.FloatCfg] :
                                          FP.FloatFP.Float
                                          Instances For
                                            unsafe def FP.ofRatUp [C : FP.FloatCfg] :
                                            FP.Float
                                            Instances For
                                              unsafe def FP.ofRatDn [C : FP.FloatCfg] (r : ) :
                                              FP.Float
                                              Instances For
                                                unsafe def FP.ofRat [C : FP.FloatCfg] :
                                                FP.RModeFP.Float
                                                Instances For
                                                  instance FP.Float.instNeg [C : FP.FloatCfg] :
                                                  Neg FP.Float
                                                  Equations
                                                  • FP.Float.instNeg = { neg := FP.Float.neg }
                                                  unsafe def FP.Float.add [C : FP.FloatCfg] (mode : FP.RMode) :
                                                  FP.FloatFP.FloatFP.Float
                                                  Instances For
                                                    unsafe instance FP.Float.instAdd [C : FP.FloatCfg] :
                                                    Add FP.Float
                                                    unsafe def FP.Float.sub [C : FP.FloatCfg] (mode : FP.RMode) (f1 : FP.Float) (f2 : FP.Float) :
                                                    FP.Float
                                                    Instances For
                                                      unsafe instance FP.Float.instSub [C : FP.FloatCfg] :
                                                      Sub FP.Float
                                                      unsafe def FP.Float.mul [C : FP.FloatCfg] (mode : FP.RMode) :
                                                      FP.FloatFP.FloatFP.Float
                                                      Instances For
                                                        unsafe def FP.Float.div [C : FP.FloatCfg] (mode : FP.RMode) :
                                                        FP.FloatFP.FloatFP.Float
                                                        Instances For