Agda.Utils.IntSet.Infinite

Possibly infinite sets of integers (but with finitely many consecutive segments). Used for checking guard coverage in int/nat cases in the treeless compiler.

Documentation

data IntSet

Represents a set of integers. Invariants: - All cannot be the argument to Below or Above - at most one IntsBelow - at most one IntsAbove - if `Below lo` and `Below hi`, then `lo < hi` - if `Below lo .. (Some xs)` then `all (> lo) xs` - if `Above hi .. (Some xs)` then `all (< hi - 1) xs`

Instances

Eq IntSet

Defined in Agda.Utils.IntSet.Infinite

Methods

(==) :: IntSet -> IntSet -> Bool

(/=) :: IntSet -> IntSet -> Bool

Show IntSet

Defined in Agda.Utils.IntSet.Infinite

Methods

showsPrec :: Int -> IntSet -> ShowS

show :: IntSet -> String

showList :: [IntSet] -> ShowS

Semigroup IntSet

Defined in Agda.Utils.IntSet.Infinite

Methods

(<>) :: IntSet -> IntSet -> IntSet

sconcat :: NonEmpty IntSet -> IntSet

stimes :: Integral b => b -> IntSet -> IntSet

Monoid IntSet

Defined in Agda.Utils.IntSet.Infinite

Methods

mempty :: IntSet

mappend :: IntSet -> IntSet -> IntSet

mconcat :: [IntSet] -> IntSet

empty :: IntSet

No integers.

full :: IntSet

All integers.

below :: Integer -> IntSet

All integers `< n`

above :: Integer -> IntSet

All integers `>= n`

singleton :: Integer -> IntSet

A single integer.

difference :: IntSet -> IntSet -> IntSet

member :: Integer -> IntSet -> Bool

Membership

toFiniteList :: IntSet -> Maybe [Integer]

If finite, return the list of elements.

invariant :: IntSet -> Bool

Invariant.