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`
ModuleAgda-2.8.0.2Haskell2010
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.
Synopsis
- data IntSet
- value empty
- value full
- value below
- value above
- value singleton
- value difference
- value member
- value toFiniteList
- value invariant
- PackageAgda-2.8.0.2
- Exports10
- LanguageHaskell2010
- LicenceMIT
- SourceInfinite.hs
No integers.
All integers.
All integers `< n`
All integers `>= n`
A single integer.
Membership
If finite, return the list of elements.
Invariant.