Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

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

Semigroup IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

Methods

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

sconcat :: NonEmpty IntSet -> IntSet

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

Show IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

Methods

showsPrec :: Int -> IntSet -> ShowS

show :: IntSet -> String

showList :: [IntSet] -> ShowS

Eq IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

Methods

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

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

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.

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

Membership

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

If finite, return the list of elements.

invariant :: IntSet -> Bool Source #

Invariant.