Implementation of floating-point numbers (experimental).

def Int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ

inductive FP.RMode : Type

• NE : RMode

def FP.instInhabitedRMode.default : RMode

@[implicit_reducible]

instance FP.instInhabitedRMode : Inhabited RMode

class FP.FloatCfg : Type

• prec : ℕ
• emax : ℕ
• precPos : 0 < prec
• precMax : prec ≤ emax

def FP.prec [C : FloatCfg] : ℕ

def FP.emax [C : FloatCfg] : ℕ

def FP.emin [C : FloatCfg] : ℤ

def FP.ValidFinite [C : FloatCfg] (e : ℤ) (m : ℕ) : Prop

@[implicit_reducible]

instance FP.instDecidableValidFinite [C : FloatCfg] (e : ℤ) (m : ℕ) : Decidable (ValidFinite e m)

inductive FP.Float [C : FloatCfg] : Type

• inf [C : FloatCfg] : Bool → Float
• nan [C : FloatCfg] : Float
• finite [C : FloatCfg] : Bool → (e : ℤ) → (m : ℕ) → ValidFinite e m → Float

def FP.Float.isFinite [C : FloatCfg] : Float → Bool

def FP.toRat [C : FloatCfg] (f : Float) : f.isFinite = true → ℚ

theorem FP.Float.Zero.valid [C : FloatCfg] : ValidFinite emin 0

def FP.Float.zero [C : FloatCfg] (s : Bool) : Float

@[implicit_reducible]

instance FP.instInhabitedFloat [C : FloatCfg] : Inhabited Float

def FP.Float.sign' [C : FloatCfg] : Float → Semiquot Bool

def FP.Float.sign [C : FloatCfg] : Float → Bool

def FP.Float.isZero [C : FloatCfg] : Float → Bool

def FP.Float.neg [C : FloatCfg] : Float → Float

def FP.divNatLtTwoPow (n d : ℕ) : ℤ → Bool

unsafe def FP.ofPosRatDn [C : FloatCfg] (n d : ℕ+) : Float × Bool

unsafe def FP.nextUpPos [C : FloatCfg] (e : ℤ) (m : ℕ) (v : ValidFinite e m) : Float

unsafe def FP.nextDnPos [C : FloatCfg] (e : ℤ) (m : ℕ) (v : ValidFinite e m) : Float

unsafe def FP.nextUp [C : FloatCfg] : Float → Float

unsafe def FP.nextDn [C : FloatCfg] : Float → Float

unsafe def FP.ofRatUp [C : FloatCfg] : ℚ → Float

unsafe def FP.ofRatDn [C : FloatCfg] (r : ℚ) : Float

unsafe def FP.ofRat [C : FloatCfg] : RMode → ℚ → Float

@[implicit_reducible]

instance FP.Float.instNeg [C : FloatCfg] : Neg Float

unsafe def FP.Float.add [C : FloatCfg] (mode : RMode) : Float → Float → Float

@[implicit_reducible]

unsafe instance FP.Float.instAdd [C : FloatCfg] : Add Float

unsafe def FP.Float.sub [C : FloatCfg] (mode : RMode) (f1 f2 : Float) : Float

@[implicit_reducible]

unsafe instance FP.Float.instSub [C : FloatCfg] : Sub Float

unsafe def FP.Float.mul [C : FloatCfg] (mode : RMode) : Float → Float → Float

unsafe def FP.Float.div [C : FloatCfg] (mode : RMode) : Float → Float → Float