mathlib3 documentation

data.fp.basic

Implementation of floating-point numbers (experimental). #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def int.shift2 (a b : ) :
Equations
@[protected, instance]
structure fp.rmode  :
Instances for fp.rmode
@[class]
structure fp.float_cfg  :
Instances for fp.float_cfg
  • fp.float_cfg.has_sizeof_inst
def fp.valid_finite [C : fp.float_cfg] (e : ) (m : ) :
Prop
Equations
Instances for fp.valid_finite
@[protected, instance]
Equations
inductive fp.float [C : fp.float_cfg] :
Instances for 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_dn [C : fp.float_cfg] (r : ) :
@[protected, instance]
Equations
@[protected, instance]
meta def fp.float.sub [C : fp.float_cfg] (mode : fp.rmode) (f1 f2 : fp.float) :
@[protected, instance]