Data.Fin.Set

Specialised set of `Fin`s.
Isomorphic to a vector of appropriate size of booleans.

This should be a replacement for `SortedSet (Fin n)` working better at least in elaborator scripts.
This can be implemented as simple `Integer` setting and clearing bits, but this seems to work worse in elaborator scripts.

Definitions

data FinSet : Nat -> Type

Totality: total
Visibility: export
Constructor: 

MkFS : Integer -> FinSet n

Hints:

Eq (FinSet n)

Interpolation (Fin n) => Interpolation (FinSet n)

Monoid (FinSet n)

Ord (FinSet n)

Semigroup (FinSet n)

Show (FinSet n)

empty : FinSet n

Totality: total
Visibility: export

full : FinSet n

Totality: total
Visibility: export

complement : FinSet n -> FinSet n

Totality: total
Visibility: export

insert : Fin n -> FinSet n -> FinSet n

Totality: total
Visibility: export

insert' : FinSet n -> Fin n -> FinSet n

Totality: total
Visibility: export

delete : Fin n -> FinSet n -> FinSet n

Totality: total
Visibility: export

delete' : FinSet n -> Fin n -> FinSet n

Totality: total
Visibility: export

contains : Fin n -> FinSet n -> Bool

Totality: total
Visibility: export

contains' : FinSet n -> Fin n -> Bool

Totality: total
Visibility: export

fromFoldable : Foldable f => f (Fin n) -> FinSet n

Totality: total
Visibility: export

fromList : List (Fin n) -> FinSet n

Totality: total
Visibility: export

toList : FinSet n -> List (Fin n)

Totality: total
Visibility: export

traverse_ : Monad m => (Fin n -> m b) -> FinSet n -> m ()

Totality: total
Visibility: export

for_ : Monad m => FinSet n -> (Fin n -> m b) -> m ()

Totality: total
Visibility: public export

foldl : (a -> Fin n -> a) -> a -> FinSet n -> a

Totality: total
Visibility: export

foldMap : Monoid m => (Fin n -> m) -> FinSet n -> m

Totality: total
Visibility: public export

.asList : FinSet n -> List (Fin n)

Totality: total
Visibility: public export

size : FinSet n -> Nat

Totality: total
Visibility: public export

.size : FinSet n -> Nat

Totality: total
Visibility: public export

.asVect : (fs : FinSet n) -> Vect (fs .size) (Fin n)

Totality: total
Visibility: public export

union : FinSet n -> FinSet n -> FinSet n

Totality: total
Visibility: export

difference : FinSet n -> FinSet n -> FinSet n

Totality: total
Visibility: export

symDifference : FinSet n -> FinSet n -> FinSet n

Totality: total
Visibility: export

intersection : FinSet n -> FinSet n -> FinSet n

Totality: total
Visibility: export

leftMost : FinSet n -> Maybe (Fin n)

Totality: total
Visibility: export

rightMost : FinSet n -> Maybe (Fin n)

Totality: total
Visibility: export

null : FinSet n -> Bool

Totality: total
Visibility: export

keySet : SortedMap (Fin n) v -> FinSet n

Totality: total
Visibility: export

keySetSize : (m : SortedMap (Fin n) v) -> (keySet m) .size = length (toList m)

Totality: total
Visibility: export

keySet : FinMap n v -> FinSet n

Totality: total
Visibility: export

keySetSize : (m : FinMap n v) -> (keySet m) .size = length (kvList m)

Totality: total
Visibility: export

toSortedSet : FinSet n -> SortedSet (Fin n)

Totality: total
Visibility: export

singleton : Fin n -> FinSet n

Totality: total
Visibility: export

fit : FinSet n -> FinSet m

Totality: total
Visibility: export

weakenToSuper : FinSet (finToNat i) -> FinSet n

Totality: total
Visibility: export