- float : Type
- val : self.float
- lt : self.float → self.float → Prop
- le : self.float → self.float → Prop
- decLt : DecidableRel self.lt
- decLe : DecidableRel self.le
Native floating point type, corresponding to the IEEE 754 binary64 format
(double
in C or f64
in Rust).
- val : floatSpec.float
Instances For
- FloatArray.instForInFloat
- FloatArray.instGetElemNatFloatLtSize
- FloatArray.instGetElemUSizeFloatLtNatValValSize
- Lean.instFromJsonFloat
- Lean.instToJsonFloat
- Rat.instCoeFloat
- instAddFloat
- instBEqFloat
- instDivFloat
- instHomogeneousPowFloat
- instInhabitedFloat
- instLEFloat
- instLTFloat
- instMaxFloat
- instMinFloat
- instMulFloat
- instNegFloat
- instOfNatFloat
- instOfScientificFloat
- instReprAtomFloat
- instReprFloat
- instSubFloat
- instToStringFloat
Equations
- instInhabitedFloat = { default := { val := floatSpec.val } }
Equations
- floatDecLt a b = a.decLt b
Equations
- floatDecLe a b = a.decLe b
If the given float is non-negative, truncates the value to the nearest non-negative integer.
If negative or NaN, returns 0
.
If larger than the maximum value for UInt8
(including Inf), returns the maximum value of UInt8
(i.e. UInt8.size - 1
).
If the given float is non-negative, truncates the value to the nearest non-negative integer.
If negative or NaN, returns 0
.
If larger than the maximum value for UInt16
(including Inf), returns the maximum value of UInt16
(i.e. UInt16.size - 1
).
If the given float is non-negative, truncates the value to the nearest non-negative integer.
If negative or NaN, returns 0
.
If larger than the maximum value for UInt32
(including Inf), returns the maximum value of UInt32
(i.e. UInt32.size - 1
).
If the given float is non-negative, truncates the value to the nearest non-negative integer.
If negative or NaN, returns 0
.
If larger than the maximum value for UInt64
(including Inf), returns the maximum value of UInt64
(i.e. UInt64.size - 1
).
If the given float is non-negative, truncates the value to the nearest non-negative integer.
If negative or NaN, returns 0
.
If larger than the maximum value for USize
(including Inf), returns the maximum value of USize
(i.e. USize.size - 1
). This value is platform dependent).
Equations
- instToStringFloat = { toString := Float.toString }
Equations
- instReprFloat = { reprPrec := fun (n : Float) (prec : Nat) => if n < UInt64.toFloat 0 then Repr.addAppParen (Std.Format.text (toString n)) prec else Std.Format.text (toString n) }
Equations
- instHomogeneousPowFloat = { pow := Float.pow }
Efficiently computes x * 2^i
.