structure Data.Scientific : Type

A number in scientific notation: $c \times 10^{e}$.

• coefficient — the significand $c$ (arbitrary-precision integer)
• base10Exponent — the exponent $e$ (arbitrary-precision integer)

Two Scientific values are logically equal when they represent the same real number; structural equality after normalize is canonical.

• coefficient : Int

  The significand $c$.

• base10Exponent : Int

  The base-10 exponent $e$.

def Data.instReprScientific.repr : Scientific → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instReprScientific : Repr Scientific

Equations

• Data.instReprScientific = { reprPrec := Data.instReprScientific.repr }

@[inline]

def Data.Scientific.scientific (c e : Int) : Scientific

Smart constructor: $\text{scientific}(c, e) = c \times 10^{e}$.

Equations

• Data.Scientific.scientific c e = { coefficient := c, base10Exponent := e }

@[inline]

def Data.Scientific.fromInt (n : Int) : Scientific

Create a Scientific from an integer: $n \mapsto n \times 10^{0}$.

Equations

• Data.Scientific.fromInt n = { coefficient := n, base10Exponent := 0 }

def Data.Scientific.normalize (s : Scientific) : Scientific

Remove trailing zeros from the coefficient, adjusting the exponent.

$$\text{normalize}(c \times 10^{e}) = (c / 10^{k}) \times 10^{e+k}$$

where $k$ is the number of trailing zeros in $c$. The result is canonical: the coefficient has no trailing zeros (or is zero).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Data.Scientific.isZero (s : Scientific) : Bool

Is the number zero? $$\text{isZero}(s) \iff c = 0$$

Equations

• s.isZero = (s.coefficient == 0)

def Data.Scientific.isInteger (s : Scientific) : Bool

Is the number an integer? True when the exponent is non-negative (after normalization).

Equations

• s.isInteger = decide (s.normalize.base10Exponent ≥ 0)

@[inline]

def Data.Scientific.isNegativeZero : Scientific → Bool

Is the number negative zero? Always false since Int has no negative zero.

Equations

• x✝.isNegativeZero = false

def Data.Scientific.toRealFloat (s : Scientific) : Float

Convert to Float (may lose precision for large or very precise values).

$$\text{toRealFloat}(c \times 10^{e}) = \text{Float.ofInt}(c) \times 10^{e}$$

Equations

• One or more equations did not get rendered due to their size.

def Data.Scientific.fromFloatDigits (f : Float) : Scientific

Convert a Float to Scientific by decomposing it into decimal digits.

Note: this performs a best-effort conversion through the string representation, similar to Haskell's fromFloatDigits.

Equations

• One or more equations did not get rendered due to their size.

def Data.Scientific.toBoundedInteger (s : Scientific) : Option Int

Convert to a bounded integer, returning none if the number is fractional or outside the representable range of a 64-bit signed integer.

Range: $[-2^{63}, 2^{63} - 1]$.

Equations

• One or more equations did not get rendered due to their size.

def Data.Scientific.toDecimalDigits (s : Scientific) : List Nat × Int

Decompose into a list of mantissa digits and a base-10 exponent.

Returns (digits, exp) such that: $$\text{value} = 0.\text{digits} \times 10^{\text{exp}}$$

For example, $123.45$ yields ([1,2,3,4,5], 3). The digit list has no trailing zeros. For zero, returns ([0], 1).

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Scientific.instAdd : Add Scientific

Equations

• Data.Scientific.instAdd = { add := fun (a b : Data.Scientific) => match Data.Scientific.align✝ a b with | (c1, c2, e) => { coefficient := c1 + c2, base10Exponent := e } }

@[implicit_reducible]

instance Data.Scientific.instSub : Sub Scientific

Equations

• Data.Scientific.instSub = { sub := fun (a b : Data.Scientific) => match Data.Scientific.align✝ a b with | (c1, c2, e) => { coefficient := c1 - c2, base10Exponent := e } }

@[implicit_reducible]

instance Data.Scientific.instMul : Mul Scientific

Equations

• Data.Scientific.instMul = { mul := fun (a b : Data.Scientific) => { coefficient := a.coefficient * b.coefficient, base10Exponent := a.base10Exponent + b.base10Exponent } }

@[implicit_reducible]

instance Data.Scientific.instNeg : Neg Scientific

Equations

• Data.Scientific.instNeg = { neg := fun (s : Data.Scientific) => { coefficient := -s.coefficient, base10Exponent := s.base10Exponent } }

@[implicit_reducible]

instance Data.Scientific.instBEq : BEq Scientific

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Scientific.instOrd : Ord Scientific

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Scientific.instInhabited : Inhabited Scientific

Equations

• Data.Scientific.instInhabited = { default := { coefficient := 0, base10Exponent := 0 } }

@[implicit_reducible]

instance Data.Scientific.instOfNat {n : Nat} : OfNat Scientific n

Equations

• Data.Scientific.instOfNat = { ofNat := { coefficient := ↑n, base10Exponent := 0 } }

@[implicit_reducible]

instance Data.Scientific.instOfScientific : OfScientific Scientific

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Scientific.instToString : ToString Scientific

Format a Scientific as a plain decimal string.

• $1.23 \times 10^{5}$ → "123000.0"
• $1.23 \times 10^{-2}$ → "0.0123"
• $-42 \times 10^{0}$ → "-42.0"

Equations

• One or more equations did not get rendered due to their size.

theorem Data.Scientific.isZero_iff (s : Scientific) : s.isZero = true ↔ s.coefficient = 0

isZero is true if and only if the coefficient is zero. $$\text{isZero}(s) = \text{true} \iff s.\text{coefficient} = 0$$

theorem Data.Scientific.isZero_fromInt_zero : (fromInt 0).isZero = true

fromInt 0 produces a zero scientific. $$\text{isZero}(\text{fromInt}(0)) = \text{true}$$

theorem Data.Scientific.normalize_zero (e : Int) : { coefficient := 0, base10Exponent := e }.normalize = { coefficient := 0, base10Exponent := 0 }

Normalizing zero yields the canonical zero ⟨0, 0⟩. $$\text{normalize}(0 \times 10^{e}) = 0 \times 10^{0}$$

theorem Data.Scientific.neg_neg (s : Scientific) : - -s = s

Negation is self-inverse. $$-(-s) = s$$

theorem Data.Scientific.fromInt_zero_beq : (fromInt 0 == 0) = true

fromInt preserves zero under BEq. $$(\text{fromInt}(0) == 0) = \text{true}$$