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

constant 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]

constant Float.add :

Float → Float → Float

source

@[extern lean_float_sub]

constant Float.sub :

Float → Float → Float

source

@[extern lean_float_mul]

constant Float.mul :

Float → Float → Float

source

@[extern lean_float_div]

constant Float.div :

Float → Float → Float

source

@[extern lean_float_negate]

constant Float.neg :

Float → Float

source

noncomputable 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

noncomputable 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]

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

Bool

source

instance instBEqFloat :

BEq Float

Equations

instBEqFloat = { beq := Float.beq }

source

@[extern lean_float_decLt]

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

Decidable (a < b)

source

@[extern lean_float_decLe]

constant 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]

constant Float.toString :

Float → String

source

@[extern lean_float_to_uint8]

constant Float.toUInt8 :

Float → UInt8

source

@[extern lean_float_to_uint16]

constant Float.toUInt16 :

Float → UInt16

source

@[extern lean_float_to_uint32]

constant Float.toUInt32 :

Float → UInt32

source

@[extern lean_float_to_uint64]

constant Float.toUInt64 :

Float → UInt64

source

@[extern lean_float_to_usize]

constant 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]

constant UInt64.toFloat (n : UInt64) :

Float

source

@[extern sin]

constant Float.sin :

Float → Float

source

@[extern cos]

constant Float.cos :

Float → Float

source

@[extern tan]

constant Float.tan :

Float → Float

source

@[extern asin]

constant Float.asin :

Float → Float

source

@[extern acos]

constant Float.acos :

Float → Float

source

@[extern atan]

constant Float.atan :

Float → Float

source

@[extern atan2]

constant Float.atan2 :

Float → Float → Float

source

@[extern sinh]

constant Float.sinh :

Float → Float

source

@[extern cosh]

constant Float.cosh :

Float → Float

source

@[extern tanh]

constant Float.tanh :

Float → Float

source

@[extern asinh]

constant Float.asinh :

Float → Float

source

@[extern acosh]

constant Float.acosh :

Float → Float

source

@[extern atanh]

constant Float.atanh :

Float → Float

source

@[extern exp]

constant Float.exp :

Float → Float

source

@[extern exp2]

constant Float.exp2 :

Float → Float

source

@[extern log]

constant Float.log :

Float → Float

source

@[extern log2]

constant Float.log2 :

Float → Float

source

@[extern log10]

constant Float.log10 :

Float → Float

source

@[extern pow]

constant Float.pow :

Float → Float → Float

source

@[extern sqrt]

constant Float.sqrt :

Float → Float

source

@[extern cbrt]

constant Float.cbrt :

Float → Float

source

instance instPowFloat :

Pow Float Float

Equations

instPowFloat = { pow := Float.pow }

source

@[extern lean_float_scaleb]

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

Float

Efficiently computes x*2^i.