structure DefinedTimeInterval : Type

• lower : PosixTime
• upper : PosixTime

instance instBEqDefinedTimeInterval : BEq DefinedTimeInterval

Equations

• instBEqDefinedTimeInterval = { beq := instBEqDefinedTimeInterval.beq }

def instBEqDefinedTimeInterval.beq : DefinedTimeInterval → DefinedTimeInterval → Bool

Equations

• instBEqDefinedTimeInterval.beq { lower := a, upper := a_1 } { lower := b, upper := b_1 } = (a == b && a_1 == b_1)
• instBEqDefinedTimeInterval.beq x✝¹ x✝ = false

structure TimeInterval : Type

• lower : Option PosixTime
• upper : Option PosixTime

instance instBEqTimeInterval : BEq TimeInterval

Equations

• instBEqTimeInterval = { beq := instBEqTimeInterval.beq }

def instBEqTimeInterval.beq : TimeInterval → TimeInterval → Bool

Equations

• instBEqTimeInterval.beq { lower := a, upper := a_1 } { lower := b, upper := b_1 } = (a == b && a_1 == b_1)
• instBEqTimeInterval.beq x✝¹ x✝ = false

def instHashableTimeInterval.hash : TimeInterval → UInt64

Equations

• instHashableTimeInterval.hash { lower := a, upper := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance instHashableTimeInterval : Hashable TimeInterval

Equations

• instHashableTimeInterval = { hash := instHashableTimeInterval.hash }

def TimeInterval.always : TimeInterval

Equations

• TimeInterval.always = { lower := none, upper := none }

def TimeInterval.valid (t : TimeInterval) : Prop

Equations

• t.valid = match t.lower, t.upper with | some ll, some uu => ll < uu | x, x_1 => True

def TimeInterval.defined (t : TimeInterval) : Prop

Equations

• t.defined = ∃ (l : PosixTime), ∃ (u : PosixTime), t.lower = some l ∧ t.upper = some u

@[reducible, inline]

abbrev LessLower (t : PosixTime) (l : Option PosixTime) : Bool

Equations

• LessLower t none = decide False
• LessLower t (some l') = decide (t < l')

def LessEqLower (l t : Option PosixTime) : Prop

Equations

• LessEqLower none t = True
• LessEqLower (some val) none = False
• LessEqLower (some l') (some t') = (l' ≤ t')

instance instDecidableLessEqLowerOfDecidableLEPosixTime {l t : Option PosixTime} [decLE : DecidableLE PosixTime] : Decidable (LessEqLower l t)

Equations

• instDecidableLessEqLowerOfDecidableLEPosixTime = isTrue True.intro
• instDecidableLessEqLowerOfDecidableLEPosixTime = isFalse instDecidableLessEqLowerOfDecidableLEPosixTime._proof_1
• instDecidableLessEqLowerOfDecidableLEPosixTime = decLE l' t'

def UndefDefTimeInclusion (l : TimeInterval) (d : DefinedTimeInterval) : Bool

Equations

• UndefDefTimeInclusion l d = match l.lower, l.upper with | some ll, some uu => decide (d.lower ≤ ll) && decide (uu < d.upper) | x, x_1 => false

def LessUpper (l t : Option PosixTime) : Prop

Equations

• LessUpper none none = True
• LessUpper none (some val) = False
• LessUpper (some l') (some t') = (l' < t')
• LessUpper (some val) none = True

instance instDecidableLessUpperOfDecidableLTPosixTime {l t : Option PosixTime} [decLT : DecidableLT PosixTime] : Decidable (LessUpper l t)

Equations

• instDecidableLessUpperOfDecidableLTPosixTime = isTrue True.intro
• instDecidableLessUpperOfDecidableLTPosixTime = isFalse instDecidableLessEqLowerOfDecidableLEPosixTime._proof_1
• instDecidableLessUpperOfDecidableLTPosixTime = isTrue True.intro
• instDecidableLessUpperOfDecidableLTPosixTime = decLT l' t'

@[reducible, inline]

abbrev IntervalInclusion (i i' : TimeInterval) : Prop

Equations

• IntervalInclusion i i' = (LessEqLower i'.lower i.lower ∧ LessUpper i.upper i'.upper)

instance instDecidableIntervalInclusionOfDecidableLTPosixTime {i i' : TimeInterval} [DecidableLT PosixTime] : Decidable (IntervalInclusion i i')

Equations

• instDecidableIntervalInclusionOfDecidableLTPosixTime = if H : decide (LessEqLower i'.lower i.lower ∧ LessUpper i.upper i'.upper) = true then isTrue ⋯ else isFalse ⋯

def TimeInclusion (e : PosixTime) (i : TimeInterval) : Prop

Equations

• TimeInclusion e i = (i.lower ≤ some e ∧ some e < i.upper)

def TimeInterval.shift (ti : TimeInterval) (sh : PosixTime) : TimeInterval

Equations

• ti.shift sh = { lower := (fun (x : PosixTime) => x + sh) <$> ti.lower, upper := (fun (x : PosixTime) => x + sh) <$> ti.upper }

instance instHasSSubsetTimeInterval : HasSSubset TimeInterval

Equations

• instHasSSubsetTimeInterval = { SSubset := IntervalInclusion }