Documentation

Std.Time.Internal.Bounded

def Std.Time.Internal.Bounded (rel : IntIntProp) (lo hi : Int) :

A Bounded is represented by an Int that is constrained by a lower and higher bounded using some relation rel. It includes all the integers that rel lo val ∧ rel val hi.

Equations
    Instances For
      @[always_inline]
      instance Std.Time.Internal.Bounded.instLE {rel : IntIntProp} {n m : Int} :
      _root_.LE (Bounded rel n m)
      Equations
        @[always_inline]
        instance Std.Time.Internal.Bounded.instLT {rel : IntIntProp} {n m : Int} :
        _root_.LT (Bounded rel n m)
        Equations
          @[always_inline]
          instance Std.Time.Internal.Bounded.instOrd {rel : IntIntProp} {n m : Int} :
          Ord (Bounded rel n m)
          Equations
            @[always_inline]
            instance Std.Time.Internal.Bounded.instRepr {rel : IntIntProp} {m n : Int} :
            Repr (Bounded rel m n)
            Equations
              @[always_inline]
              instance Std.Time.Internal.Bounded.instDecidableEq {rel : IntIntProp} {n m : Int} :
              Equations
                @[always_inline]
                instance Std.Time.Internal.Bounded.instDecidableLe {rel : IntIntProp} {a b : Int} {x y : Bounded rel a b} :
                Equations
                  instance Std.Time.Internal.Bounded.instTransOrd {rel : IntIntProp} {n m : Int} :
                  TransOrd (Bounded rel n m)
                  @[reducible, inline]

                  A Bounded integer that the relation used is the the less-equal relation so, it includes all integers that lo ≤ val ≤ hi.

                  Equations
                    Instances For
                      @[inline]
                      def Std.Time.Internal.Bounded.cast {rel : IntIntProp} {lo₁ lo₂ hi₁ hi₂ : Int} (h₁ : lo₁ = lo₂) (h₂ : hi₁ = hi₂) (b : Bounded rel lo₁ hi₁) :
                      Bounded rel lo₂ hi₂

                      Casts the boundaries of the Bounded using equivalences.

                      Equations
                        Instances For
                          @[reducible, inline]

                          A Bounded integer that the relation used is the the less-than relation so, it includes all integers that lo < val < hi.

                          Equations
                            Instances For
                              @[inline]
                              def Std.Time.Internal.Bounded.mk {lo hi : Int} {rel : IntIntProp} (val : Int) (proof : rel lo val rel val hi) :
                              Bounded rel lo hi

                              Creates a new Bounded Integer.

                              Equations
                                Instances For
                                  @[inline]
                                  def Std.Time.Internal.Bounded.ofInt? {rel : IntIntProp} {lo hi : Int} [DecidableRel rel] (val : Int) :
                                  Option (Bounded rel lo hi)

                                  Convert a Int to a Bounded if it checks.

                                  Equations
                                    Instances For
                                      @[inline]
                                      def Std.Time.Internal.Bounded.LE.ofNatWrapping {lo hi : Int} (val : Int) (h : lo hi) :
                                      LE lo hi

                                      Convert a Nat to a Bounded.LE by wrapping it.

                                      Equations
                                        Instances For
                                          instance Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast {lo : Int} {n k : Nat} :
                                          OfNat (LE lo (lo + k)) n
                                          Equations
                                            Equations
                                              @[inline]
                                              def Std.Time.Internal.Bounded.LE.mk {lo hi : Int} (val : Int) (proof : lo val val hi) :
                                              LE lo hi

                                              Creates a new Bounded integer that the relation is less-equal.

                                              Equations
                                                Instances For
                                                  @[inline]
                                                  def Std.Time.Internal.Bounded.LE.exact (val : Nat) :
                                                  LE val val

                                                  Creates a new Bounded integer that the relation is less-equal.

                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def Std.Time.Internal.Bounded.LE.ofInt {lo hi : Int} (val : Int) :
                                                      Option (LE lo hi)

                                                      Creates a new Bounded integer.

                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          def Std.Time.Internal.Bounded.LE.ofNat {hi : Nat} (val : Nat) (h : val hi) :
                                                          LE 0 hi

                                                          Convert a Nat to a Bounded.LE.

                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              def Std.Time.Internal.Bounded.LE.ofNat? {hi : Nat} (val : Nat) :
                                                              Option (LE 0 hi)

                                                              Convert a Nat to a Bounded.LE if it checks.

                                                              Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Std.Time.Internal.Bounded.LE.ofNat' {lo hi : Nat} (val : Nat) (h : lo val val hi) :
                                                                  LE lo hi

                                                                  Convert a Nat to a Bounded.LE using the lower boundary too.

                                                                  Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      def Std.Time.Internal.Bounded.LE.clip {lo hi : Int} (val : Int) (h : lo hi) :
                                                                      LE lo hi

                                                                      Convert a Nat to a Bounded.LE using the lower boundary too.

                                                                      Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Std.Time.Internal.Bounded.LE.toNat {lo hi : Int} (n : LE lo hi) :

                                                                          Convert a Bounded.LE to a Nat.

                                                                          Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Std.Time.Internal.Bounded.LE.toNat' {lo hi : Int} (n : LE lo hi) (h : lo 0) :

                                                                              Convert a Bounded.LE to a Nat.

                                                                              Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Std.Time.Internal.Bounded.LE.toInt {lo hi : Int} (n : LE lo hi) :

                                                                                  Convert a Bounded.LE to an Int.

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Std.Time.Internal.Bounded.LE.toFin {lo hi : Int} (n : LE lo hi) (h₀ : 0 lo) :
                                                                                      Fin (hi + 1).toNat

                                                                                      Convert a Bounded.LE to a Fin.

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Std.Time.Internal.Bounded.LE.ofFin {hi : Nat} (fin : Fin hi.succ) :
                                                                                          LE 0 hi

                                                                                          Convert a Fin to a Bounded.LE.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Std.Time.Internal.Bounded.LE.ofFin' {hi lo : Nat} (fin : Fin hi.succ) (h : lo hi) :
                                                                                              LE lo hi

                                                                                              Convert a Fin to a Bounded.LE.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Std.Time.Internal.Bounded.LE.byEmod (b i : Int) (hi : i > 0) :
                                                                                                  LE 0 (i - 1)

                                                                                                  Creates a new Bounded.LE using a the modulus of a number.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      def Std.Time.Internal.Bounded.LE.byMod (b i : Int) (hi : 0 < i) :
                                                                                                      LE (-(i - 1)) (i - 1)

                                                                                                      Creates a new Bounded.LE using a the Truncating modulus of a number.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          def Std.Time.Internal.Bounded.LE.truncate {n m : Int} (bounded : LE n m) :
                                                                                                          LE 0 (m - n)

                                                                                                          Adjust the bounds of a Bounded by setting the lower bound to zero and the maximum value to (m - n).

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Std.Time.Internal.Bounded.LE.truncateTop {n m j : Int} (bounded : LE n m) (h : bounded.val j) :
                                                                                                              LE n j

                                                                                                              Adjust the bounds of a Bounded by changing the higher bound if another value j satisfies the same constraint.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Std.Time.Internal.Bounded.LE.truncateBottom {n m j : Int} (bounded : LE n m) (h : bounded.val j) :
                                                                                                                  LE j m

                                                                                                                  Adjust the bounds of a Bounded by changing the lower bound if another value j satisfies the same constraint.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Std.Time.Internal.Bounded.LE.neg {n m : Int} (bounded : LE n m) :
                                                                                                                      LE (-m) (-n)

                                                                                                                      Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Std.Time.Internal.Bounded.LE.add {n m : Int} (bounded : LE n m) (num : Int) :
                                                                                                                          LE (n + num) (m + num)

                                                                                                                          Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def Std.Time.Internal.Bounded.LE.addProven {n m num : Int} (bounded : LE n m) (h₀ : bounded.val + num m) (h₁ : num 0) :
                                                                                                                              LE n m

                                                                                                                              Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  def Std.Time.Internal.Bounded.LE.addTop {n m : Int} (bounded : LE n m) (num : Int) (h : num 0) :
                                                                                                                                  LE n (m + num)

                                                                                                                                  Adjust the bounds of a Bounded by adding a constant value to the upper bounds.

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      @[inline]
                                                                                                                                      def Std.Time.Internal.Bounded.LE.subBottom {n m : Int} (bounded : LE n m) (num : Int) (h : num 0) :
                                                                                                                                      LE (n - num) m

                                                                                                                                      Adjust the bounds of a Bounded by adding a constant value to the lower bounds.

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          def Std.Time.Internal.Bounded.LE.addBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) :
                                                                                                                                          LE (n + i) (m + j)

                                                                                                                                          Adds two Bounded and adjust the boundaries.

                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              @[inline]
                                                                                                                                              def Std.Time.Internal.Bounded.LE.sub {n m : Int} (bounded : LE n m) (num : Int) :
                                                                                                                                              LE (n - num) (m - num)

                                                                                                                                              Adjust the bounds of a Bounded by subtracting a constant value to both the lower and upper bounds.

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[inline]
                                                                                                                                                  def Std.Time.Internal.Bounded.LE.subBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) :
                                                                                                                                                  LE (n - j) (m - i)

                                                                                                                                                  Adds two Bounded and adjust the boundaries.

                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Std.Time.Internal.Bounded.LE.emod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) :
                                                                                                                                                      LE 0 (num✝ - 1)

                                                                                                                                                      Adjust the bounds of a Bounded by applying the emod operation constraining the lower bound to 0 and the upper bound to the value.

                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Std.Time.Internal.Bounded.LE.mod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) :
                                                                                                                                                          LE (-(num✝ - 1)) (num✝ - 1)

                                                                                                                                                          Adjust the bounds of a Bounded by applying the mod operation.

                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              def Std.Time.Internal.Bounded.LE.mul_pos {n m : Int} (bounded : LE n m) (num : Int) (h : num 0) :
                                                                                                                                                              LE (n * num) (m * num)

                                                                                                                                                              Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  def Std.Time.Internal.Bounded.LE.mul_neg {n m : Int} (bounded : LE n m) (num : Int) (h : num 0) :
                                                                                                                                                                  LE (m * num) (n * num)

                                                                                                                                                                  Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      def Std.Time.Internal.Bounded.LE.ediv {n m : Int} (bounded : LE n m) (num : Int) (h : num > 0) :
                                                                                                                                                                      LE (n / num) (m / num)

                                                                                                                                                                      Adjust the bounds of a Bounded by applying the div operation.

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              def Std.Time.Internal.Bounded.LE.expand {lo hi nhi nlo : Int} (bounded : LE lo hi) (h : hi nhi) (h₁ : nlo lo) :
                                                                                                                                                                              LE nlo nhi

                                                                                                                                                                              Expand the range of a bounded value.

                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  def Std.Time.Internal.Bounded.LE.expandTop {lo hi nhi : Int} (bounded : LE lo hi) (h : hi nhi) :
                                                                                                                                                                                  LE lo nhi

                                                                                                                                                                                  Expand the bottom of the bounded to a number nhi is hi is less or equal to the previous higher bound.

                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      def Std.Time.Internal.Bounded.LE.expandBottom {lo hi nlo : Int} (bounded : LE lo hi) (h : nlo lo) :
                                                                                                                                                                                      LE nlo hi

                                                                                                                                                                                      Expand the bottom of the bounded to a number nlo if lo is greater or equal to the previous lower bound.

                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          def Std.Time.Internal.Bounded.LE.succ {lo hi : Int} (bounded : LE lo hi) (h : bounded.val < hi) :
                                                                                                                                                                                          LE lo hi

                                                                                                                                                                                          Adds one to the value of the bounded if the value is less than the higher bound of the bounded number.

                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              def Std.Time.Internal.Bounded.LE.abs {i : Int} (bo : LE (-i) i) :
                                                                                                                                                                                              LE 0 i

                                                                                                                                                                                              Returns the absolute value of the bounded number bo with bounds -(i - 1) to i - 1. The result will be a new bounded number with bounds 0 to i - 1.

                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def Std.Time.Internal.Bounded.LE.max {n m : Int} (bounded : LE n m) (val : Int) :
                                                                                                                                                                                                  LE (Max.max n val) (Max.max m val)

                                                                                                                                                                                                  Returns the maximum between a number and the bounded.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For