Implementation of floating-point numbers (experimental). #
- inf: [C : FP.FloatCfg] → Bool → FP.Float
- nan: [C : FP.FloatCfg] → FP.Float
- finite: [C : FP.FloatCfg] → Bool → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float
Instances For
Instances For
Instances For
Instances For
unsafe def
FP.Float.sub
[C : FP.FloatCfg]
(mode : FP.RMode)
(f1 : FP.Float)
(f2 : FP.Float)
:
FP.Float