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.

Instances For
@[always_inline]
instance Std.Time.Internal.Bounded.instLE {rel : IntIntProp} {n m : Int} :
Equations
@[always_inline]
instance Std.Time.Internal.Bounded.instLT {rel : IntIntProp} {n m : Int} :
Equations
@[always_inline]
@[always_inline]
instance Std.Time.Internal.Bounded.instBEq {rel : IntIntProp} {n m : Int} :
@[always_inline]
instance Std.Time.Internal.Bounded.instDecidableLe {rel : IntIntProp} {a b : Int} {x y : Std.Time.Internal.Bounded rel a b} :
@[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 : Std.Time.Internal.Bounded rel lo₁ hi₁) :

Casts the boundaries of the Bounded using equivalences.

Equations
@[reducible, inline]

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

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

Creates a new Bounded Integer.

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

Convert a Int to a Bounded if it checks.

Equations
@[inline]

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

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

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

Equations
@[inline]

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

@[inline]

Creates a new Bounded integer.

Equations
@[inline]

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

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

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

@[inline]

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

Equations
@[inline]

Convert a Bounded.LE to a Nat.

@[inline]

Convert a Bounded.LE to a Nat.

@[inline]

Convert a Bounded.LE to an Int.

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

Convert a Bounded.LE to a Fin.

Equations
  • n.toFin h₀ = n.val.toNat,
@[inline]

Convert a Fin to a Bounded.LE.

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

Convert a Fin to a Bounded.LE.

@[inline]

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

Equations
@[inline]

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

@[inline]

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

Equations
  • bounded.truncate = match with | => bounded.val - n,
@[inline]

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

Equations
  • bounded.truncateTop h = bounded.val,
@[inline]

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

@[inline]

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

@[inline]

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

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

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

Equations
  • bounded.addProven h₀ h₁ = bounded.val + num,
@[inline]

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

Equations
  • bounded.addTop num h = bounded.val + num,
@[inline]

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

@[inline]

Adds two Bounded and adjust the boundaries.

@[inline]

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

Equations
  • bounded.sub num = bounded.add (-num)
@[inline]

Adds two Bounded and adjust the boundaries.

Equations
  • bounded.subBounds bounded₂ = bounded.addBounds bounded₂.neg
@[inline]
def Std.Time.Internal.Bounded.LE.emod {n num : Int} (bounded : Std.Time.Internal.Bounded.LE n num) (num✝ : Int) (hi : 0 < num✝) :

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
@[inline]
def Std.Time.Internal.Bounded.LE.mod {n num : Int} (bounded : Std.Time.Internal.Bounded.LE n num) (num✝ : Int) (hi : 0 < num✝) :
Std.Time.Internal.Bounded.LE (-(num✝ - 1)) (num✝ - 1)

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

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

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

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

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

Equations
  • bounded.mul_neg num h = bounded.val * num,
@[inline]
def Std.Time.Internal.Bounded.LE.ediv {n m : Int} (bounded : Std.Time.Internal.Bounded.LE n m) (num : Int) (h : num > 0) :

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

Equations
  • bounded.ediv num h = match with | => bounded.val.ediv num,
@[inline]
Equations
  • Std.Time.Internal.Bounded.LE.eq = n,
@[inline]
def Std.Time.Internal.Bounded.LE.expand {lo hi nhi nlo : Int} (bounded : Std.Time.Internal.Bounded.LE lo hi) (h : hi nhi) (h₁ : nlo lo) :

Expand the range of a bounded value.

Equations
  • bounded.expand h h₁ = bounded.val,
@[inline]

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

Equations
  • bounded.expandTop h = bounded.expand h
@[inline]

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

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

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

@[inline]

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
  • bo.abs = if h : bo.val 0 then bo.truncateBottom h else let r := (bo.truncateTop ).neg; .mp r

Returns the maximum between a number and the bounded.