Interval Set

IntervalSet operations like IntervalSet.canonicalize or IntervalSet.intersection

def IntervalSet.Acc.with_none (acc : Interval.Acc) (n : NonemptyInterval Char) (h : acc.next.isNone = true) : Interval.Acc

Equations

• IntervalSet.Acc.with_none acc n h = { next := some n, set := acc.set, nonOverlapping := ⋯ }

def IntervalSet.Acc.with_next (acc : Interval.Acc) (n : NonemptyInterval Char) (h1 : Interval.is_start_eq acc.next n) : Interval.Acc

Equations

• IntervalSet.Acc.with_next acc n h1 = { next := some n, set := acc.set, nonOverlapping := ⋯ }

def IntervalSet.Acc.with_next_set (acc : Interval.Acc) (l r : NonemptyInterval Char) (h1 : Interval.nonOverlapping l r) (h2 : acc.next = some l) : Interval.Acc

Equations

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

instance IntervalSet.instInhabitedAcc : Inhabited Interval.Acc

Equations

• IntervalSet.instInhabitedAcc = { default := { next := none, set := default, nonOverlapping := IntervalSet.instInhabitedAcc.proof_1 } }

def IntervalSet.canonicalize (ranges : Array (NonemptyInterval Char)) : IntervalSet Char

Converts ranges into IntervalSet with canonical ordering.

Equations

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

def IntervalSet.negate (interval : IntervalSet Char) : IntervalSet Char

Negate a interval set wrt the corresponding BoundedOrder instBoundedOrderCharInstLEChar .

Equations

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

def IntervalSet.intersection (interval1 interval2 : IntervalSet Char) : IntervalSet Char

Intersection of interval sets

Equations

• interval1.intersection interval2 = IntervalSet.canonicalize (IntervalSet.intersection.loop 0 0 interval1.intervals interval2.intervals #[])

@[irreducible]

def IntervalSet.intersection.loop (a b : Nat) (ra rb acc : Array (NonemptyInterval Char)) : Array (NonemptyInterval Char)

Equations

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

def IntervalSet.difference (interval1 interval2 : IntervalSet Char) : IntervalSet Char

Subtract the interval set interval2 from interval1.

Equations

• interval1.difference interval2 = interval1.intersection interval2.negate

def IntervalSet.union (interval1 interval2 : IntervalSet Char) : IntervalSet Char

Union of interval sets.

Equations

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

def IntervalSet.symmetric_difference (interval1 interval2 : IntervalSet Char) : IntervalSet Char

Compute the symmetric difference (A⊖B = (A∪B)(A∩B)) of the two sets.

Equations

• interval1.symmetric_difference interval2 = (interval1.union interval2).difference (interval1.intersection interval2)