HepLean Documentation

Init.Data.Float

structure FloatSpec :

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

Instances For

opaque floatSpec :

structure Float :

Native floating point type, corresponding to the IEEE 754 binary64 format (double in C or f64 in Rust).

val : floatSpec.float

Instances For

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

Float → Float → Prop

Equations

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

Instances For

Float → Float → Prop

Equations

a.le b = floatSpec.le a.val b.val

Instances For

instance instAddFloat :

Equations

instAddFloat = { add := Float.add }

instance instSubFloat :

Equations

instSubFloat = { sub := Float.sub }

instance instMulFloat :

Equations

instMulFloat = { mul := Float.mul }

instance instDivFloat :

Equations

instDivFloat = { div := Float.div }

instance instNegFloat :

Equations

instNegFloat = { neg := Float.neg }

instance instLTFloat :

Equations

instLTFloat = { lt := Float.lt }

instance instLEFloat :

Equations

instLEFloat = { le := Float.le }

@[extern lean_float_beq]

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

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

instance instBEqFloat :

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 = a.decLt b

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

Decidable (a ≤ b)

Equations

floatDecLe a b = a.decLe 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 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).

@[extern lean_float_to_uint16]

opaque Float.toUInt16 :

Float → UInt16

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).

@[extern lean_float_to_uint32]

opaque Float.toUInt32 :

Float → UInt32

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).

@[extern lean_float_to_uint64]

opaque Float.toUInt64 :

Float → UInt64

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).

@[extern lean_float_to_usize]

opaque Float.toUSize :

Float → USize

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).

@[extern lean_float_isnan]

opaque Float.isNaN :

@[extern lean_float_isfinite]

opaque Float.isFinite :

@[extern lean_float_isinf]

opaque Float.isInf :

@[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 :

Equations

instToStringFloat = { toString := Float.toString }

@[extern lean_uint64_to_float]

opaque UInt64.toFloat (n : UInt64) :

instance instReprFloat :

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) }

instance instReprAtomFloat :

Equations

instReprAtomFloat = { }

@[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 instHomogeneousPowFloat :

HomogeneousPow Float

Equations

instHomogeneousPowFloat = { pow := Float.pow }

instance instMinFloat :

Equations

instMinFloat = minOfLe

instance instMaxFloat :

Equations

instMaxFloat = maxOfLe

@[extern lean_float_scaleb]

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

Efficiently computes x * 2^i.