Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.IntSet.Infinite

Description

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

Synopsis

- data IntSet
- empty :: IntSet
- full :: IntSet
- below :: Integer -> IntSet
- above :: Integer -> IntSet
- singleton :: Integer -> IntSet
- difference :: IntSet -> IntSet -> IntSet
- member :: Integer -> IntSet -> Bool
- toFiniteList :: IntSet -> Maybe [Integer]
- invariant :: IntSet -> Bool

# Documentation

data IntSet Source #

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

Instances details

Monoid IntSet Source # |
Instance details Defined in Agda.Utils.IntSet.Infinite Methods mempty :: IntSet Source # mappend :: IntSet -> IntSet -> IntSet Source # mconcat :: [IntSet] -> IntSet Source #
Semigroup IntSet Source # |
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (<>) :: IntSet -> IntSet -> IntSet Source # sconcat :: NonEmpty IntSet -> IntSet Source # stimes :: Integral b => b -> IntSet -> IntSet Source #
Show IntSet Source # |
Instance details Defined in Agda.Utils.IntSet.Infinite Methods showsPrec :: Int -> IntSet -> ShowS Source # show :: IntSet -> String Source # showList :: [IntSet] -> ShowS Source #
Eq IntSet Source # |
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (==) :: IntSet -> IntSet -> Bool Source # (/=) :: IntSet -> IntSet -> Bool Source #

empty :: IntSet Source #

No integers.

full :: IntSet Source #

All integers.

below :: Integer -> IntSet Source #

All integers `< n`

above :: Integer -> IntSet Source #

All integers `>= n`

singleton :: Integer -> IntSet Source #

A single integer.

difference :: IntSet -> IntSet -> IntSet Source #

member :: Integer -> IntSet -> Bool Source #

Membership

toFiniteList :: IntSet -> Maybe [Integer] Source #

If finite, return the list of elements.

invariant :: IntSet -> Bool Source #

Invariant.