mathlib documentation

data.fp.basic

source
def int.shift2 (a b : ℕ) (a_1 : ℤ) :
ℕ × ℕ

Equations
source
@[instance]
def fp.rmode.inhabited  :
inhabited fp.rmode

source
inductive fp.rmode  :
Type

source
@[class]
structure fp.float_cfg  :
Type

source
def fp.prec [C : fp.float_cfg] :
ℕ

Equations
source
def fp.emax [C : fp.float_cfg] :
ℕ

Equations
source
def fp.emin [C : fp.float_cfg] :
ℤ

Equations
source
def fp.valid_finite [C : fp.float_cfg] (e : ℤ) (m : ℕ) :
Prop

Equations
source
@[instance]
def fp.dec_valid_finite [C : fp.float_cfg] (e : ℤ) (m : ℕ) :
decidable (fp.valid_finite e m)

Equations
source
inductive fp.float [C : fp.float_cfg] :
Type

source
def fp.float.is_finite [C : fp.float_cfg] (a : fp.float) :
bool

Equations
source
def fp.to_rat [C : fp.float_cfg] (f : fp.float) (a : ↥(f.is_finite)) :
ℚ

Equations
source
theorem fp.float.zero.valid [C : fp.float_cfg] :
fp.valid_finite fp.emin 0

source
def fp.float.zero [C : fp.float_cfg] (s : bool) :
fp.float

Equations
source
@[instance]
def fp.inhabited [C : fp.float_cfg] :
inhabited fp.float

Equations
source
def fp.float.sign' [C : fp.float_cfg] (a : fp.float) :
semiquot bool

Equations
source
def fp.float.sign [C : fp.float_cfg] (a : fp.float) :
bool

Equations
source
def fp.float.is_zero [C : fp.float_cfg] (a : fp.float) :
bool

Equations
source
def fp.float.neg [C : fp.float_cfg] (a : fp.float) :
fp.float

Equations
source
def fp.div_nat_lt_two_pow [C : fp.float_cfg] (n d : ℕ) (a : ℤ) :
bool

Equations
source
meta def fp.of_pos_rat_dn [C : fp.float_cfg] (n d : ℕ+) :
fp.float × bool

source
meta def fp.next_up_pos [C : fp.float_cfg] (e : ℤ) (m : ℕ) (v : fp.valid_finite e m) :
fp.float

source
meta def fp.next_dn_pos [C : fp.float_cfg] (e : ℤ) (m : ℕ) (v : fp.valid_finite e m) :
fp.float

source
meta def fp.next_up [C : fp.float_cfg] (a : fp.float) :
fp.float

source
meta def fp.next_dn [C : fp.float_cfg] (a : fp.float) :
fp.float

source
meta def fp.of_rat_up [C : fp.float_cfg] (a : ℚ) :
fp.float

source
meta def fp.of_rat_dn [C : fp.float_cfg] (r : ℚ) :
fp.float

source
meta def fp.of_rat [C : fp.float_cfg] (a : fp.rmode) (a_1 : ℚ) :
fp.float

source
@[instance]
def fp.float.has_neg [C : fp.float_cfg] :
has_neg fp.float

Equations
source
meta def fp.float.add [C : fp.float_cfg] (mode : fp.rmode) (a a_1 : fp.float) :
fp.float

source
@[instance]
meta def fp.float.has_add [C : fp.float_cfg] :
has_add fp.float

source
meta def fp.float.sub [C : fp.float_cfg] (mode : fp.rmode) (f1 f2 : fp.float) :
fp.float

source
@[instance]
meta def fp.float.has_sub [C : fp.float_cfg] :
has_sub fp.float

source
meta def fp.float.mul [C : fp.float_cfg] (mode : fp.rmode) (a a_1 : fp.float) :
fp.float

source
meta def fp.float.div [C : fp.float_cfg] (mode : fp.rmode) (a a_1 : fp.float) :
fp.float