Implementation of floating-point numbers (experimental). #
Equations
- int.shift2 a b -[1+ e] = (a, b.shiftl e.succ)
- int.shift2 a b (int.of_nat e) = (a.shiftl e, b)
@[class]
- prec : ℕ
- emax : ℕ
- prec_pos : 0 < fp.float_cfg.prec
- prec_max : fp.float_cfg.prec ≤ fp.float_cfg.emax
Instances for fp.float_cfg
- fp.float_cfg.has_sizeof_inst
@[protected, instance]
Equations
- fp.dec_valid_finite e m = _.mpr and.decidable
- inf : Π [C : fp.float_cfg], bool → fp.float
- nan : Π [C : fp.float_cfg], fp.float
- finite : Π [C : fp.float_cfg], bool → Π (e : ℤ) (m : ℕ), fp.valid_finite e m → fp.float
Instances for fp.float
- fp.float.has_sizeof_inst
- fp.float.inhabited
- fp.float.has_neg
- fp.float.has_add
- fp.float.has_sub
Equations
- (fp.float.finite s e m f).is_finite = bool.tt
- fp.float.nan.is_finite = bool.ff
- (fp.float.inf ᾰ).is_finite = bool.ff
Equations
- fp.to_rat (fp.float.finite s e m f) _x = fp.to_rat._match_1 s (int.shift2 m 1 e)
- fp.to_rat._match_1 s (n, d) = let r : ℚ := rat.mk_nat ↑n d in ite ↥s (-r) r
Equations
@[protected, instance]
Equations
@[protected]
Equations
- (fp.float.finite s e m f).sign' = has_pure.pure s
- fp.float.nan.sign' = ⊤
- (fp.float.inf s).sign' = has_pure.pure s
@[protected]
Equations
- (fp.float.finite s e m f).sign = s
- fp.float.nan.sign = bool.ff
- (fp.float.inf s).sign = s
@[protected]
Equations
- (fp.float.finite ᾰ e n.succ ᾰ_1).is_zero = bool.ff
- (fp.float.finite s e 0 f).is_zero = bool.tt
- fp.float.nan.is_zero = bool.ff
- (fp.float.inf ᾰ).is_zero = bool.ff
@[protected]
Equations
- (fp.float.finite s e m f).neg = fp.float.finite (!s) e m f
- fp.float.nan.neg = fp.float.nan
- (fp.float.inf s).neg = fp.float.inf (!s)
Equations
- fp.div_nat_lt_two_pow n d -[1+ e] = decidable.to_bool (n.shiftl e.succ < d)
- fp.div_nat_lt_two_pow n d (int.of_nat e) = decidable.to_bool (n < d.shiftl e)
@[protected, instance]
Equations
- fp.float.has_neg = {neg := fp.float.neg C}