Documentation

Time.Fixed

theorem Time.Fixed.ext {precision : Nat} {x : Time.Fixed precision} {y : Time.Fixed precision} (val : x.val = y.val) :

x = y

theorem Time.Fixed.ext_iff {precision : Nat} {x : Time.Fixed precision} {y : Time.Fixed precision} :

x = y ↔ x.val = y.val

structure Time.Fixed (precision : Nat) :

fixed-point representation of a fractional number

val : Int

Instances For

instance Time.instReprFixed :

{precision : Nat} → Repr (Time.Fixed precision)

Equations

Time.instReprFixed = { reprPrec := Time.reprFixed✝ }

instance Time.instBEqFixed :

{precision : Nat} → BEq (Time.Fixed precision)

Equations

Time.instBEqFixed = { beq := Time.beqFixed✝ }

instance Time.instDecidableEqFixed :

{precision : Nat} → DecidableEq (Time.Fixed precision)

Equations

Time.instDecidableEqFixed = Time.decEqFixed✝

inductive Time.Sign :

Nonneg: Time.Sign
Neg: Time.Sign

Instances For

instance Time.instReprSign :

Equations

Time.instReprSign = { reprPrec := Time.reprSign✝ }

instance Time.instBEqSign :

Equations

Time.instBEqSign = { beq := Time.beqSign✝ }

instance Time.instDecidableEqSign :

DecidableEq Time.Sign

Equations

Time.instDecidableEqSign x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure Time.Fixed.Denominator (precision : Nat) :

denominator of Fixed p

val : Nat
lt : self.val < 10 ^ precision

Instances For

theorem Time.Fixed.Denominator.lt {precision : Nat} (self : Time.Fixed.Denominator precision) :

self.val < 10 ^ precision

instance Time.Fixed.instReprDenominator :

{precision : Nat} → Repr (Time.Fixed.Denominator precision)

Equations

Time.Fixed.instReprDenominator = { reprPrec := Time.Fixed.reprDenominator✝ }

instance Time.Fixed.instBEqDenominator :

{precision : Nat} → BEq (Time.Fixed.Denominator precision)

Equations

Time.Fixed.instBEqDenominator = { beq := Time.Fixed.beqDenominator✝ }

instance Time.Fixed.instDecidableEqDenominator :

{precision : Nat} → DecidableEq (Time.Fixed.Denominator precision)

Equations

Time.Fixed.instDecidableEqDenominator = Time.Fixed.decEqDenominator✝

structure Time.Fixed.Parts (precision : Nat) :

parts of Fixed p

sign : Time.Sign
numerator : Nat
denominator : Nat
lt : self.denominator < 10 ^ precision

Instances For

theorem Time.Fixed.Parts.lt {precision : Nat} (self : Time.Fixed.Parts precision) :

self.denominator < 10 ^ precision

instance Time.Fixed.instReprParts :

{precision : Nat} → Repr (Time.Fixed.Parts precision)

Equations

Time.Fixed.instReprParts = { reprPrec := Time.Fixed.reprParts✝ }

instance Time.Fixed.instBEqParts :

{precision : Nat} → BEq (Time.Fixed.Parts precision)

Equations

Time.Fixed.instBEqParts = { beq := Time.Fixed.beqParts✝ }

instance Time.Fixed.instDecidableEqParts :

{precision : Nat} → DecidableEq (Time.Fixed.Parts precision)

Equations

Time.Fixed.instDecidableEqParts = Time.Fixed.decEqParts✝

def Time.Fixed.zero {p : Nat} :

Equations

Time.Fixed.zero = { val := 0 }

Instances For

def Time.Fixed.Denominator.zero {p : Nat} :

Time.Fixed.Denominator p

Equations

Time.Fixed.Denominator.zero = { val := 0, lt := ⋯ }

Instances For

instance Time.instInhabitedFixed {p : Nat} :

Inhabited (Time.Fixed p)

Equations

Time.instInhabitedFixed = { default := Time.Fixed.zero }

instance Time.instLTFixed {p : Nat} :

LT (Time.Fixed p)

Equations

Time.instLTFixed = { lt := fun (a b : Time.Fixed p) => a.val < b.val }

theorem Time.lt_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

(a < b) = (a.val < b.val)

instance Time.instLEFixed {p : Nat} :

LE (Time.Fixed p)

Equations

Time.instLEFixed = { le := fun (a b : Time.Fixed p) => a.val ≤ b.val }

instance Time.instLeReflFixed {p : Nat} :

Time.LeRefl (Time.Fixed p)

Equations

Time.instLeReflFixed = { le_refl := ⋯ }

theorem Time.le_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

(a ≤ b) = (a.val ≤ b.val)

instance Time.instInhabitedDenominator {p : Nat} :

Inhabited (Time.Fixed.Denominator p)

Equations

Time.instInhabitedDenominator = { default := Time.Fixed.Denominator.zero }

theorem Time.inhabited_def {p : Nat} :

default = Time.Fixed.Denominator.zero

instance Time.instLTDenominator {p : Nat} :

LT (Time.Fixed.Denominator p)

Equations

Time.instLTDenominator = { lt := fun (a b : Time.Fixed.Denominator p) => a.val < b.val }

instance Time.instLEDenominator {p : Nat} :

LE (Time.Fixed.Denominator p)

Equations

Time.instLEDenominator = { le := fun (a b : Time.Fixed.Denominator p) => a.val ≤ b.val }

instance Time.instLeReflDenominator {p : Nat} :

Time.LeRefl (Time.Fixed.Denominator p)

Equations

Time.instLeReflDenominator = { le_refl := ⋯ }

def Time.Fixed.neg {p : Nat} (f : Time.Fixed p) :

Equations

f.neg = { val := -f.val }

Instances For

def Time.Fixed.toParts {p : Nat} (f : Time.Fixed p) :

Time.Fixed.Parts p

Equations

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

Instances For

def Time.Fixed.toFixed {p : Nat} (sign : Time.Sign) (num : Nat) (denom : Time.Fixed.Denominator p) :

Equations

Time.Fixed.toFixed sign num denom = { val := match sign with | Time.Sign.Neg => Int.negOfNat (num * 10 ^ p + denom.val) | Time.Sign.Nonneg => ↑num * 10 ^ p + ↑denom.val }

Instances For

def Time.Fixed.Parts.fromParts {p : Nat} (parts : Time.Fixed.Parts p) :

Equations

parts.fromParts = Time.Fixed.toFixed parts.sign parts.numerator { val := parts.denominator, lt := ⋯ }

Instances For

def Time.Fixed.toSign (n : Int) :

Equations

Time.Fixed.toSign n = if n < 0 then Time.Sign.Neg else Time.Sign.Nonneg

Instances For

def Time.Fixed.toDenominator (n : Nat) (p : Nat) :

Time.Fixed.Denominator p

remove trailing digits untill n < 10 ^ p

Equations

Time.Fixed.toDenominator n p = let_fun h := ⋯; let s := Time.Fixed.toDenominator.clip_denom n (10 ^ p) h; { val := s.val, lt := ⋯ }

Instances For

@[irreducible]

def Time.Fixed.toDenominator.clip_denom (n : Nat) (p : Nat) (hp : 0 < p) :

{ n : Nat // n < p }

Equations

Time.Fixed.toDenominator.clip_denom n p hp = if h : 0 < n then if h1 : n ≥ p then Time.Fixed.toDenominator.clip_denom (n / 10) p hp else ⟨n, ⋯⟩ else ⟨0, hp⟩

Instances For

def Time.Fixed.denominatorValueToString (d : Int) (p : Nat) :

Equations

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

Instances For

def Time.Fixed.denominatorToString {p : Nat} (f : Time.Fixed p) :

Equations

f.denominatorToString = match f.toParts with | { sign := sign, numerator := numerator, denominator := d, lt := lt } => Time.Fixed.denominatorValueToString (↑d) p

Instances For

instance Time.Fixed.instToString {p : Nat} :

ToString (Time.Fixed p)

Equations

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

def Time.Fixed.sub {p : Nat} (dt1 : Time.Fixed p) (dt2 : Time.Fixed p) :

Equations

dt1.sub dt2 = { val := dt1.val - dt2.val }

Instances For

def Time.Fixed.add {p : Nat} (dt1 : Time.Fixed p) (dt2 : Time.Fixed p) :

Equations

dt1.add dt2 = { val := dt1.val + dt2.val }

Instances For

instance Time.Fixed.instSub {p : Nat} :

Sub (Time.Fixed p)

Equations

Time.Fixed.instSub = { sub := Time.Fixed.sub }

theorem Time.Fixed.sub_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

a - b = a.sub b

instance Time.Fixed.instAdd {p : Nat} :

Add (Time.Fixed p)

Equations

Time.Fixed.instAdd = { add := Time.Fixed.add }

theorem Time.Fixed.add_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

a + b = a.add b

def Time.Fixed.Int.toFixed (n : Int) (p : Nat) :

Equations

Time.Fixed.Int.toFixed n p = { val := n }

Instances For

def Time.Fixed.div {p : Nat} (dt1 : Time.Fixed p) (dt2 : Time.Fixed p) :

Equations

dt1.div dt2 = dt1.val / dt2.val

Instances For

instance Time.Fixed.instHDivInt {p : Nat} :

HDiv (Time.Fixed p) (Time.Fixed p) Int

Equations

Time.Fixed.instHDivInt = { hDiv := Time.Fixed.div }

theorem Time.Fixed.div_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

a / b = a.div b

def Time.Fixed.mul {p : Nat} (a : Int) (f : Time.Fixed p) :

Equations

Time.Fixed.mul a f = { val := a * f.val }

Instances For

instance Time.Fixed.instHMulInt {p : Nat} :

HMul Int (Time.Fixed p) (Time.Fixed p)

Equations

Time.Fixed.instHMulInt = { hMul := Time.Fixed.mul }

theorem Time.Fixed.mul_def {p : Nat} (a : Int) (b : Time.Fixed p) :

a * b = Time.Fixed.mul a b

def Time.Fixed.mod {p : Nat} (dt1 : Time.Fixed p) (dt2 : Time.Fixed p) :

Equations

dt1.mod dt2 = { val := dt1.val % dt2.val }

Instances For

instance Time.Fixed.instMod {p : Nat} :

Mod (Time.Fixed p)

Equations

Time.Fixed.instMod = { mod := Time.Fixed.mod }

theorem Time.Fixed.mod_def {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

a % b = a.mod b

@[simp]

theorem Time.Fixed.ofFixed_lt {p : Nat} {a : Time.Fixed p} {b : Time.Fixed p} :

a < b ↔ a.val < b.val

@[simp]

theorem Time.Fixed.ofFixed_ne {p : Nat} {a : Time.Fixed p} {b : Time.Fixed p} :

a ≠ b ↔ a.val ≠ b.val

theorem Time.Fixed.ne_of_lt {p : Nat} {a : Time.Fixed p} {b : Time.Fixed p} (h : a < b) :

a ≠ b

theorem Time.Fixed.emod_nonneg {p : Nat} (a : Time.Fixed p) {b : Time.Fixed p} (h : b ≠ { val := 0 }) :

{ val := 0 } ≤ a % b

theorem Time.Fixed.emod_lt_of_pos {p : Nat} (a : Time.Fixed p) {b : Time.Fixed p} (h : { val := 0 } < b) :

a % b < b

theorem Time.Fixed.emod_add_ediv {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) :

a % b + a / b * b = a

def Time.Fixed.toMod {p : Nat} (n : Time.Fixed p) (d : Time.Fixed p) (h : Time.Fixed.zero < d) :

{ m : Time.Fixed p // Time.Fixed.zero ≤ m ∧ m < d }

toMod computes n % d : { m : Fixed p // zero ≤ m ∧ m < d }

Equations

n.toMod d h = ⟨n % d, ⋯⟩

Instances For

theorem Time.Fixed.toFixed_lt_toFixed (p : Nat) (n : Nat) (n_denom : Time.Fixed.Denominator p) (m : Nat) (m_denom : Time.Fixed.Denominator p) (hnm : n < m) :

Time.Fixed.toFixed Time.Sign.Nonneg n n_denom < Time.Fixed.toFixed Time.Sign.Nonneg m m_denom

theorem Time.Fixed.zero_lt_toFixed (p : Nat) (m : Nat) (m_denom : Time.Fixed.Denominator p) (h : 0 < m) :

Time.Fixed.zero < Time.Fixed.toFixed Time.Sign.Nonneg m m_denom

theorem Time.Fixed.toFixed_le_toFixed_of_lt (p : Nat) (n : Nat) (n_denom : Time.Fixed.Denominator p) (m : Nat) (m_denom : Time.Fixed.Denominator p) (hnm : n < m) :

Time.Fixed.toFixed Time.Sign.Nonneg n n_denom ≤ Time.Fixed.toFixed Time.Sign.Nonneg m m_denom

theorem Time.Fixed.zero_le_toFixed (p : Nat) (m : Nat) (m_denom : Time.Fixed.Denominator p) (hnm : 0 < m) :

Time.Fixed.zero ≤ Time.Fixed.toFixed Time.Sign.Nonneg m m_denom

theorem Time.Fixed.fixed_eq_toParts_fromParts {p : Nat} (f : Time.Fixed p) :

f = f.toParts.fromParts