def Time.zeroLPad (s : String) (n : Nat) : String

Equations

• Time.zeroLPad s n = "".pushn '0' (n - s.length) ++ s

def Time.zeroRPad (s : String) (n : Nat) : String

Equations

• Time.zeroRPad s n = s ++ "".pushn '0' (n - s.length)

class Time.ToZeroPadded (α : Type u) : Type u

• toZeroPadded : α → Nat → String

instance Time.instToZeroPaddedInt : Time.ToZeroPadded Int

Equations

• Time.instToZeroPaddedInt = { toZeroPadded := fun (n : Int) (i : Nat) => Time.zeroLPad (toString (if n < 0 then -n else n)) i }

instance Time.instToZeroPaddedIccNat {a : Nat} {b : Nat} : Time.ToZeroPadded (Time.Icc a b)

Equations

• Time.instToZeroPaddedIccNat = { toZeroPadded := fun (n : Time.Icc a b) (i : Nat) => Time.zeroLPad (toString n.val) i }

instance Time.instToZeroPaddedNat : Time.ToZeroPadded Nat

Equations

• Time.instToZeroPaddedNat = { toZeroPadded := fun (n i : Nat) => Time.zeroLPad (toString n) i }