Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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

Show IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

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.