mathlib documentation

data.fp.basic

def int.shift2  :
×

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

meta def fp.next_dn_pos [C : fp.float_cfg] (e : ) (m : ) :

meta def fp.of_rat_up [C : fp.float_cfg] :

meta def fp.of_rat_dn [C : fp.float_cfg] :

meta def fp.of_rat [C : fp.float_cfg] :

@[instance]

@[instance]