structure FloatSpec : Type 1

• float : Type
• val : float
• lt : float → float → Prop
• le : float → float → Prop
• decLt : DecidableRel lt
• decLe : DecidableRel le

opaque floatSpec : FloatSpec

structure Float : Type

• val : floatSpec.float

instance instInhabitedFloat : Inhabited Float

Equations

• instInhabitedFloat = { default := { val := floatSpec.val } }

@[extern lean_float_add]

opaque Float.add : Float → Float → Float

@[extern lean_float_sub]

opaque Float.sub : Float → Float → Float

@[extern lean_float_mul]

opaque Float.mul : Float → Float → Float

@[extern lean_float_div]

opaque Float.div : Float → Float → Float

@[extern lean_float_negate]

opaque Float.neg : Float → Float

def Float.lt : Float → Float → Prop

Equations

• Float.lt a b = match a, b with | { val := a }, { val := b } => FloatSpec.lt floatSpec a b

def Float.le : Float → Float → Prop

Equations

• Float.le a b = FloatSpec.le floatSpec a.val b.val

instance instAddFloat : Add Float

Equations

• instAddFloat = { add := Float.add }

instance instSubFloat : Sub Float

Equations

• instSubFloat = { sub := Float.sub }

instance instMulFloat : Mul Float

Equations

• instMulFloat = { mul := Float.mul }

instance instDivFloat : Div Float

Equations

• instDivFloat = { div := Float.div }

instance instNegFloat : Neg Float

Equations

• instNegFloat = { neg := Float.neg }

instance instLTFloat : LT Float

Equations

• instLTFloat = { lt := Float.lt }

instance instLEFloat : LE Float

Equations

• instLEFloat = { le := Float.le }

@[extern lean_float_beq]

opaque Float.beq (a : Float) (b : Float) : Bool

Note: this is not reflexive since NaN != NaN.

instance instBEqFloat : BEq Float

Equations

• instBEqFloat = { beq := Float.beq }

@[extern lean_float_decLt]

opaque Float.decLt (a : Float) (b : Float) : Decidable (a < b)

@[extern lean_float_decLe]

opaque Float.decLe (a : Float) (b : Float) : Decidable (a ≤ b)

instance floatDecLt (a : Float) (b : Float) : Decidable (a < b)

Equations

• floatDecLt a b = Float.decLt a b

instance floatDecLe (a : Float) (b : Float) : Decidable (a ≤ b)

Equations

• floatDecLe a b = Float.decLe a b

@[extern lean_float_to_string]

opaque Float.toString : Float → String

@[extern lean_float_to_uint8]

opaque Float.toUInt8 : Float → UInt8

If the given float is positive, truncates the value to the nearest positive integer. If negative or larger than the maximum value for UInt8, returns 0.

@[extern lean_float_to_uint16]

opaque Float.toUInt16 : Float → UInt16

If the given float is positive, truncates the value to the nearest positive integer. If negative or larger than the maximum value for UInt16, returns 0.

@[extern lean_float_to_uint32]

opaque Float.toUInt32 : Float → UInt32

If the given float is positive, truncates the value to the nearest positive integer. If negative or larger than the maximum value for UInt32, returns 0.

@[extern lean_float_to_uint64]

opaque Float.toUInt64 : Float → UInt64

If the given float is positive, truncates the value to the nearest positive integer. If negative or larger than the maximum value for UInt64, returns 0.

@[extern lean_float_to_usize]

opaque Float.toUSize : Float → USize

If the given float is positive, truncates the value to the nearest positive integer. If negative or larger than the maximum value for USize, returns 0.

@[extern lean_float_isnan]

opaque Float.isNaN : Float → Bool

@[extern lean_float_isfinite]

opaque Float.isFinite : Float → Bool

@[extern lean_float_isinf]

opaque Float.isInf : Float → Bool

@[extern lean_float_frexp]

opaque Float.frExp : Float → Float × Int

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s ∈ (-1;-0.5] ∪ [0.5; 1). Returns an undefined value if x is not finite.

instance instToStringFloat : ToString Float

Equations

• instToStringFloat = { toString := Float.toString }

instance instReprFloat : Repr Float

Equations

• instReprFloat = { reprPrec := fun n x => Std.Format.text (Float.toString n) }

instance instReprAtomFloat : ReprAtom Float

Equations

• instReprAtomFloat = { }

@[extern lean_uint64_to_float]

opaque UInt64.toFloat (n : UInt64) : Float

@[extern sin]

opaque Float.sin : Float → Float

@[extern cos]

opaque Float.cos : Float → Float

@[extern tan]

opaque Float.tan : Float → Float

@[extern asin]

opaque Float.asin : Float → Float

@[extern acos]

opaque Float.acos : Float → Float

@[extern atan]

opaque Float.atan : Float → Float

@[extern atan2]

opaque Float.atan2 : Float → Float → Float

@[extern sinh]

opaque Float.sinh : Float → Float

@[extern cosh]

opaque Float.cosh : Float → Float

@[extern tanh]

opaque Float.tanh : Float → Float

@[extern asinh]

opaque Float.asinh : Float → Float

@[extern acosh]

opaque Float.acosh : Float → Float

@[extern atanh]

opaque Float.atanh : Float → Float

@[extern exp]

opaque Float.exp : Float → Float

@[extern exp2]

opaque Float.exp2 : Float → Float

@[extern log]

opaque Float.log : Float → Float

@[extern log2]

opaque Float.log2 : Float → Float

@[extern log10]

opaque Float.log10 : Float → Float

@[extern pow]

opaque Float.pow : Float → Float → Float

@[extern sqrt]

opaque Float.sqrt : Float → Float

@[extern cbrt]

opaque Float.cbrt : Float → Float

@[extern ceil]

opaque Float.ceil : Float → Float

@[extern floor]

opaque Float.floor : Float → Float

@[extern round]

opaque Float.round : Float → Float

@[extern fabs]

opaque Float.abs : Float → Float

instance instPowFloat : Pow Float Float

Equations

• instPowFloat = { pow := Float.pow }

instance instMinFloat : Min Float

Equations

• instMinFloat = minOfLe

instance instMaxFloat : Max Float

Equations

• instMaxFloat = maxOfLe

@[extern lean_float_scaleb]

opaque Float.scaleB (x : Float) (i : Int) : Float

Efficiently computes x * 2^i.