mathlib documentation

data.fp.basic

Implementation of floating-point numbers (experimental). #

def int.shift2 (a b : ) :
Equations
inductive fp.rmode  :
Type
@[class]
structure fp.float_cfg  :
Type
@[instance]
Equations
inductive fp.float [C : fp.float_cfg] :
Type
def fp.to_rat [C : fp.float_cfg] (f : fp.float) :
Equations
meta def fp.next_up_pos [C : fp.float_cfg] (e : ) (m : ) (v : fp.valid_finite e m) :
meta def fp.next_dn_pos [C : fp.float_cfg] (e : ) (m : ) (v : fp.valid_finite e m) :
meta def fp.of_rat_up [C : fp.float_cfg] :
meta def fp.of_rat_dn [C : fp.float_cfg] (r : ) :
meta def fp.of_rat [C : fp.float_cfg] :
meta def fp.float.add [C : fp.float_cfg] (mode : fp.rmode) :
@[instance]
meta def fp.float.sub [C : fp.float_cfg] (mode : fp.rmode) (f1 f2 : fp.float) :
@[instance]
meta def fp.float.mul [C : fp.float_cfg] (mode : fp.rmode) :
meta def fp.float.div [C : fp.float_cfg] (mode : fp.rmode) :