Structures · Data types
FP.FloatCfg
This class has no docstring in Mathlib.
- Defined in
- Mathlib.Data.FP.Basic
- Shape
- 0 explicit arguments · adds prec, emax, precPos, precMax
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- FP.ValidFinite
- FP.FloatCfg.prec
- FP.FloatCfg.emax
- FP.emin
- FP.FloatCfg.precMax
- FP.emax
- FP.prec
- FP.FloatCfg.precPos
- FP.Float.sign'
- FP.Float.instSub
- FP.nextDn
- FP.Float.instNeg
- FP.nextUpPos
- FP.Float.Zero.valid
- FP.nextUp
- FP.Float.nan.elim
- FP.instDecidableValidFinite
- FP.Float.neg
- FP.ofRatUp
- FP.Float.add
- FP.ofRat
- FP.toRat
- FP.Float.ctorElimType
- FP.Float.mul
- FP.Float.div
- FP.Float.isZero
- FP.Float.isFinite
- FP.Float.instAdd
- FP.ofPosRatDn
- FP.ofRatDn
- FP.Float.sub
- FP.instInhabitedFloat
- FP.Float.finite.elim
- FP.Float.zero
- FP.Float.inf.elim
- FP.nextDnPos
- FP.Float.ctorElim
- FP.Float.sign
Ancestors0
No ancestors.