Init.Data.Float

source

structure FloatSpec:

Type 1

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

source

opaque floatSpec:

FloatSpec

source

structure Float:

Type

val : floatSpec.float

source

instance instInhabitedFloat:

Inhabited Float

Equations

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

source

@[extern lean_float_add]

opaque Float.add:

Float → Float → Float

source

@[extern lean_float_sub]

opaque Float.sub:

Float → Float → Float

source

@[extern lean_float_mul]

opaque Float.mul:

Float → Float → Float

source

@[extern lean_float_div]

opaque Float.div:

Float → Float → Float

source

@[extern lean_float_negate]

opaque Float.neg:

Float → Float

source

def Float.lt:

Float → Float → Prop

Equations

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

source

def Float.le:

Float → Float → Prop

Equations

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

source

instance instAddFloat:

Add Float

Equations

instAddFloat = { add := Float.add }

source

instance instSubFloat:

Sub Float

Equations

instSubFloat = { sub := Float.sub }

source

instance instMulFloat:

Mul Float

Equations

instMulFloat = { mul := Float.mul }

source

instance instDivFloat:

Div Float

Equations

instDivFloat = { div := Float.div }

source

instance instNegFloat:

Neg Float

Equations

instNegFloat = { neg := Float.neg }

source

instance instLTFloat:

LT Float

Equations

instLTFloat = { lt := Float.lt }

source

instance instLEFloat:

LE Float

Equations

instLEFloat = { le := Float.le }

source

@[extern lean_float_beq]

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

Bool

source

instance instBEqFloat:

BEq Float

Equations

instBEqFloat = { beq := Float.beq }

source

@[extern lean_float_decLt]

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

Decidable (a < b)

source

@[extern lean_float_decLe]

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

Decidable (a ≤ b)

source

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

Decidable (a < b)

Equations

floatDecLt a b = Float.decLt a b

source

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

Decidable (a ≤ b)

Equations

floatDecLe a b = Float.decLe a b

source

@[extern lean_float_to_string]

opaque Float.toString:

Float → String

source

@[extern lean_float_to_uint8]

opaque Float.toUInt8:

Float → UInt8

source

@[extern lean_float_to_uint16]

opaque Float.toUInt16:

Float → UInt16

source

@[extern lean_float_to_uint32]

opaque Float.toUInt32:

Float → UInt32

source

@[extern lean_float_to_uint64]

opaque Float.toUInt64:

Float → UInt64

source

@[extern lean_float_to_usize]

opaque Float.toUSize:

Float → USize

source

instance instToStringFloat:

ToString Float

Equations

instToStringFloat = { toString := Float.toString }

source

instance instReprFloat:

Repr Float

Equations

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

source

instance instReprAtomFloat:

ReprAtom Float

Equations

instReprAtomFloat = { }

source

@[extern lean_uint64_to_float]

opaque UInt64.toFloat (n : UInt64) :

Float

source

@[extern sin]

opaque Float.sin:

Float → Float

source

@[extern cos]

opaque Float.cos:

Float → Float

source

@[extern tan]

opaque Float.tan:

Float → Float

source

@[extern asin]

opaque Float.asin:

Float → Float

source

@[extern acos]

opaque Float.acos:

Float → Float

source

@[extern atan]

opaque Float.atan:

Float → Float

source

@[extern atan2]

opaque Float.atan2:

Float → Float → Float

source

@[extern sinh]

opaque Float.sinh:

Float → Float

source

@[extern cosh]

opaque Float.cosh:

Float → Float

source

@[extern tanh]

opaque Float.tanh:

Float → Float

source

@[extern asinh]

opaque Float.asinh:

Float → Float

source

@[extern acosh]

opaque Float.acosh:

Float → Float

source

@[extern atanh]

opaque Float.atanh:

Float → Float

source

@[extern exp]

opaque Float.exp:

Float → Float

source

@[extern exp2]

opaque Float.exp2:

Float → Float

source

@[extern log]

opaque Float.log:

Float → Float

source

@[extern log2]

opaque Float.log2:

Float → Float

source

@[extern log10]

opaque Float.log10:

Float → Float

source

@[extern pow]

opaque Float.pow:

Float → Float → Float

source

@[extern sqrt]

opaque Float.sqrt:

Float → Float

source

@[extern cbrt]

opaque Float.cbrt:

Float → Float

source

instance instPowFloat:

Pow Float Float

Equations

instPowFloat = { pow := Float.pow }

source

@[extern lean_float_scaleb]

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

Float

Efficiently computes x * 2^i.