def Time.Clip.clipToNonemptyIcc (a : Nat) (b : Nat) (x : Int) (h : a ≤ b) : Time.NonemptyIcc a b

Equations

• Time.Clip.clipToNonemptyIcc a b x h = let x'' := x.toNat; let icc := if ha : x'' < a then ⟨a, ⋯⟩ else if hb : x'' > b then ⟨b, ⋯⟩ else ⟨x'', ⋯⟩; Time.toNonemptyIcc icc h

def Time.Clip.clip (a : Nat) (b : Nat) (x : Int) (h : a ≤ b) : Nat

Equations

• Time.Clip.clip a b x h = (Time.Clip.clipToNonemptyIcc a b x h).icc.val

def Time.Clip.clipToNonemptyIcc? (a : Nat) (b : Nat) (x : Int) (h : a ≤ b) : Option (Time.NonemptyIcc a b)

Equations

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

def Time.Clip.clipToNonemptyIco? (a : Nat) (b : Nat) (x : Int) (h : a < b) : Option (Time.NonemptyIco a b)

Equations

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

def Time.Clip.clip? (a : Nat) (b : Nat) (x : Int) (h : a ≤ b) : Option Nat

Equations

• Time.Clip.clip? a b x h = Option.map (fun (v : Time.NonemptyIcc a b) => v.icc.val) (Time.Clip.clipToNonemptyIcc? a b x h)

def Time.Clip.clipToIco? {p : Nat} (a : Time.Fixed p) (b : Time.Fixed p) (x : Time.Fixed p) : Option (Time.Ico a b)

Equations

• Time.Clip.clipToIco? a b x = if ha : a.val ≤ x.val then if hb : x.val < b.val then some ⟨x, ⋯⟩ else none else none