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) :