Documentation

Time.Fixed

structure Time.Fixed (precision : Nat) :

fixed-point representation of a fractional number

Instances For
    theorem Time.Fixed.ext_iff {precision : Nat} {x y : Fixed precision} :
    x = y x.val = y.val
    theorem Time.Fixed.ext {precision : Nat} {x y : Fixed precision} (val : x.val = y.val) :
    x = y
    instance Time.instReprFixed {precision✝ : Nat} :
    Repr (Fixed precision✝)
    Equations
    instance Time.instBEqFixed {precision✝ : Nat} :
    BEq (Fixed precision✝)
    Equations
    inductive Time.Sign :
    Instances For
      Equations
      structure Time.Fixed.Denominator (precision : Nat) :

      denominator of Fixed p

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

        parts of Fixed p

        Instances For
          instance Time.Fixed.instReprParts {precision✝ : Nat} :
          Repr (Parts precision✝)
          Equations
          instance Time.Fixed.instBEqParts {precision✝ : Nat} :
          BEq (Parts precision✝)
          Equations
          Equations
          Instances For
            Equations
            Instances For
              instance Time.instLTFixed {p : Nat} :
              LT (Fixed p)
              Equations
              theorem Time.lt_def {p : Nat} (a b : Fixed p) :
              (a < b) = (a.val < b.val)
              instance Time.instLEFixed {p : Nat} :
              LE (Fixed p)
              Equations
              theorem Time.le_def {p : Nat} (a b : Fixed p) :
              (a b) = (a.val b.val)
              def Time.Fixed.neg {p : Nat} (f : Fixed p) :
              Equations
              Instances For
                def Time.Fixed.toParts {p : Nat} (f : Fixed p) :
                Equations
                Instances For
                  def Time.Fixed.toFixed {p : Nat} (sign : Sign) (num : Nat) (denom : Denominator p) :
                  Equations
                  Instances For
                    def Time.Fixed.Parts.fromParts {p : Nat} (parts : Parts p) :
                    Equations
                    Instances For
                      def Time.Fixed.toDenominator (n p : Nat) (h : n < 10 ^ p) :
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            def Time.Fixed.sub {p : Nat} (dt1 dt2 : Fixed p) :
                            Equations
                            Instances For
                              def Time.Fixed.add {p : Nat} (dt1 dt2 : Fixed p) :
                              Equations
                              Instances For
                                theorem Time.Fixed.sub_def {p : Nat} (a b : Fixed p) :
                                a - b = a.sub b
                                theorem Time.Fixed.add_def {p : Nat} (a b : Fixed p) :
                                a + b = a.add b
                                def Time.Fixed.Int.toFixed (n : Int) (p : Nat) :
                                Equations
                                Instances For
                                  def Time.Fixed.div {p : Nat} (dt1 dt2 : Fixed p) :
                                  Equations
                                  Instances For
                                    theorem Time.Fixed.div_def {p : Nat} (a b : Fixed p) :
                                    a / b = a.div b
                                    def Time.Fixed.mul {p : Nat} (a : Int) (f : Fixed p) :
                                    Equations
                                    Instances For
                                      theorem Time.Fixed.mul_def {p : Nat} (a : Int) (b : Fixed p) :
                                      a * b = mul a b
                                      def Time.Fixed.mod {p : Nat} (dt1 dt2 : Fixed p) :
                                      Equations
                                      Instances For
                                        theorem Time.Fixed.mod_def {p : Nat} (a b : Fixed p) :
                                        a % b = a.mod b
                                        @[simp]
                                        theorem Time.Fixed.ofFixed_lt {p : Nat} {a b : Fixed p} :
                                        a < b a.val < b.val
                                        @[simp]
                                        theorem Time.Fixed.ofFixed_ne {p : Nat} {a b : Fixed p} :
                                        a b a.val b.val
                                        theorem Time.Fixed.ne_of_lt {p : Nat} {a b : Fixed p} (h : a < b) :
                                        a b
                                        theorem Time.Fixed.emod_nonneg {p : Nat} (a : Fixed p) {b : Fixed p} (h : b { val := 0 }) :
                                        { val := 0 } a % b
                                        theorem Time.Fixed.emod_lt_of_pos {p : Nat} (a : Fixed p) {b : Fixed p} (h : { val := 0 } < b) :
                                        a % b < b
                                        theorem Time.Fixed.emod_add_ediv {p : Nat} (a b : Fixed p) :
                                        a % b + a / b * b = a
                                        def Time.Fixed.toMod {p : Nat} (n d : Fixed p) (h : zero < d) :
                                        { m : Fixed p // zero m m < d }

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

                                        Equations
                                        Instances For
                                          theorem Time.Fixed.toFixed_lt_toFixed (p n : Nat) (n_denom : Denominator p) (m : Nat) (m_denom : Denominator p) (hnm : n < m) :
                                          theorem Time.Fixed.zero_lt_toFixed (p m : Nat) (m_denom : Denominator p) (h : 0 < m) :
                                          theorem Time.Fixed.toFixed_le_toFixed_of_lt (p n : Nat) (n_denom : Denominator p) (m : Nat) (m_denom : Denominator p) (hnm : n < m) :
                                          theorem Time.Fixed.zero_le_toFixed (p m : Nat) (m_denom : Denominator p) (hnm : 0 < m) :