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

Equations

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

def Time.Clip.clip (a 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 b : Nat) (x : Int) (h : a ≤ b) : Option (NonemptyIcc a b)

Equations

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

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

Equations

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

def Time.Clip.clip? (a 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 b x : Fixed p) : Option (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