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.7.0.1Haskell2010
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.
- 1 type
- 9 values
- PackageAgda-2.7.0.1
- 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.