Implementation of floating-point numbers (experimental).

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

inductive FP.RMode : Type

• NE: FP.RMode

instance FP.instInhabitedRMode : Inhabited FP.RMode

class FP.FloatCfg : Type

• prec : ℕ
• emax : ℕ
• precPos : 0 < FP.FloatCfg.prec
• precMax : FP.FloatCfg.prec ≤ FP.FloatCfg.emax

def FP.prec [C : FP.FloatCfg] : ℕ

def FP.emax [C : FP.FloatCfg] : ℕ

def FP.emin [C : FP.FloatCfg] : ℤ

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

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

inductive FP.Float [C : FP.FloatCfg] : Type

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

unsafe instance FP.Float.instAddFloat [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

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

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

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