structure Data.Fixed (precision : Nat) : Type

A fixed-point decimal number with precision decimal places.

The underlying representation is a scaled integer: $$\text{Fixed}_p(v) \equiv v \times 10^{-p}$$

The precision $p$ is a type parameter, so Fixed 2 $\neq$ Fixed 4. This prevents accidental mixing of different precisions at compile time.

For example, Fixed 2 represents values like $3.14$ (stored as $314$).

• raw : Int

  The raw scaled integer. The actual value is $\text{raw} \times 10^{-\text{precision}}$.

def Data.instBEqFixed.beq {precision✝ : Nat} : Fixed precision✝ → Fixed precision✝ → Bool

Equations

• Data.instBEqFixed.beq { raw := a } { raw := b } = (a == b)
• Data.instBEqFixed.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqFixed {precision✝ : Nat} : BEq (Fixed precision✝)

Equations

• Data.instBEqFixed = { beq := Data.instBEqFixed.beq }

def Data.instOrdFixed.ord {precision✝ : Nat} : Fixed precision✝ → Fixed precision✝ → Ordering

Equations

• Data.instOrdFixed.ord { raw := a } { raw := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instOrdFixed {precision✝ : Nat} : Ord (Fixed precision✝)

Equations

• Data.instOrdFixed = { compare := Data.instOrdFixed.ord }

def Data.instReprFixed.repr {precision✝ : Nat} : Fixed precision✝ → Nat → Std.Format

Equations

• Data.instReprFixed.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "raw" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.raw)).group) " }"

@[implicit_reducible]

instance Data.instReprFixed {precision✝ : Nat} : Repr (Fixed precision✝)

Equations

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

@[implicit_reducible]

instance Data.instHashableFixed {precision✝ : Nat} : Hashable (Fixed precision✝)

Equations

• Data.instHashableFixed = { hash := Data.instHashableFixed.hash }

def Data.instHashableFixed.hash {precision✝ : Nat} : Fixed precision✝ → UInt64

Equations

• Data.instHashableFixed.hash { raw := a } = mixHash 0 (hash a)

def Data.Fixed.scale (p : Nat) : Nat

Compute $10^n$ as a natural number. Helper for scaling operations. $$\text{scale}(p) = 10^p$$

Equations

• Data.Fixed.scale p = Nat.pow 10 p

theorem Data.Fixed.scale_pos (p : Nat) : scale p > 0

Proof that $10^p > 0$ for any $p$.

@[inline]

def Data.Fixed.fromInt {p : Nat} (n : Int) : Fixed p

Create a Fixed from an integer (no fractional part). $$\text{fromInt}(n) = n \times 10^p \times 10^{-p} = n$$

Equations

• Data.Fixed.fromInt n = { raw := n * ↑(Data.Fixed.scale p) }

@[implicit_reducible]

instance Data.Fixed.instAdd {p : Nat} : Add (Fixed p)

Addition of fixed-point numbers (exact, no precision loss): $$\text{Fixed}_p(a) + \text{Fixed}_p(b) = \text{Fixed}_p(a + b)$$

Equations

• Data.Fixed.instAdd = { add := fun (a b : Data.Fixed p) => { raw := a.raw + b.raw } }

@[implicit_reducible]

instance Data.Fixed.instSub {p : Nat} : Sub (Fixed p)

Subtraction of fixed-point numbers (exact, no precision loss): $$\text{Fixed}_p(a) - \text{Fixed}_p(b) = \text{Fixed}_p(a - b)$$

Equations

• Data.Fixed.instSub = { sub := fun (a b : Data.Fixed p) => { raw := a.raw - b.raw } }

@[implicit_reducible]

instance Data.Fixed.instNeg {p : Nat} : Neg (Fixed p)

Negation: $-\text{Fixed}_p(a) = \text{Fixed}_p(-a)$.

Equations

• Data.Fixed.instNeg = { neg := fun (a : Data.Fixed p) => { raw := -a.raw } }

@[implicit_reducible]

instance Data.Fixed.instMul {p : Nat} : Mul (Fixed p)

Multiplication scales by $10^{-p}$ to maintain precision: $$\text{Fixed}_p(a) \times \text{Fixed}_p(b) = \text{Fixed}_p\!\left(\left\lfloor \frac{a \cdot b}{10^p} \right\rfloor\right)$$

Note: multiplication may lose precision in the last digit due to truncation.

Equations

• Data.Fixed.instMul = { mul := fun (a b : Data.Fixed p) => { raw := a.raw * b.raw / ↑(Data.Fixed.scale p) } }

@[implicit_reducible]

instance Data.Fixed.instOfNatOfNatNat {p : Nat} : OfNat (Fixed p) 0

Equations

• Data.Fixed.instOfNatOfNatNat = { ofNat := { raw := 0 } }

@[implicit_reducible]

instance Data.Fixed.instOfNatOfNatNat_1 {p : Nat} : OfNat (Fixed p) 1

Equations

• Data.Fixed.instOfNatOfNatNat_1 = { ofNat := { raw := ↑(Data.Fixed.scale p) } }

@[implicit_reducible]

instance Data.Fixed.instInhabited {p : Nat} : Inhabited (Fixed p)

Equations

• Data.Fixed.instInhabited = { default := 0 }

@[implicit_reducible]

instance Data.Fixed.instToString {p : Nat} : ToString (Fixed p)

Equations

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

theorem Data.Fixed.add_exact {p : Nat} (a b : Fixed p) : (a + b).raw = a.raw + b.raw

Addition is exact: adding two fixed-point values and converting to ratio equals converting each to ratio and adding.

$$\text{toRatio}(a + b) = \text{toRatio}(a) + \text{toRatio}(b)$$

This is the key advantage of fixed-point over floating-point: addition introduces no rounding error.

theorem Data.Fixed.sub_exact {p : Nat} (a b : Fixed p) : (a - b).raw = a.raw - b.raw

Subtraction is also exact: $$\text{toRatio}(a - b) = \text{toRatio}(a) - \text{toRatio}(b)$$

theorem Data.Fixed.neg_neg {p : Nat} (a : Fixed p) : - -a = a

Double negation: $-(-a) = a$.

theorem Data.Fixed.fromInt_zero {p : Nat} : (fromInt 0).raw = 0

fromInt 0 yields zero raw value when precision is nonzero.

def Data.Fixed.toRatio {p : Nat} (f : Fixed p) : Ratio

Convert to a Ratio preserving the exact value: $$\text{toRatio}(\text{Fixed}_p(v)) = \frac{v}{10^p}$$

Equations

• f.toRatio = Data.Ratio.mk' f.raw ↑(Data.Fixed.scale p) ⋯