Idris2Doc : Data.List.Set

Data.List.Set

(source)

Definitions

recordListSet : Type->Type
Totality: total
Visibility: public export
Constructor: 
MkListSet : Eqv=>Listv->ListSetv

Projections:
.eq : ListSetv->Eqv
.rawValues : ListSetv->Listv

Hints:
FoldableListSet
Ordk=>Monoid (ListSetk)
Ordk=>Semigroup (ListSetk)
Showk=>Show (ListSetk)
.eq : ListSetv->Eqv
Visibility: public export
eq : ListSetv->Eqv
Visibility: public export
.rawValues : ListSetv->Listv
Visibility: public export
rawValues : ListSetv->Listv
Visibility: public export
empty : Eqv=>ListSetv
Visibility: export
insert : v->ListSetv->ListSetv
Visibility: export
insert' : ListSetv->v->ListSetv
Visibility: public export
contains : v->ListSetv->Bool
Visibility: export
contains' : ListSetv->v->Bool
Visibility: public export
singleton : Eqv=>v->ListSetv
Visibility: export
fromList : Eqv=>Listv->ListSetv
Visibility: export
normalise : ListSetv->ListSetv
Visibility: export
.asList : ListSetv->Listv
Visibility: export
union : ListSetv->ListSetv->ListSetv
  Set union. Keeps the equality specified by the left set.

Visibility: export
difference : ListSetv->ListSetv->ListSetv
  Set difference. Delete all elements in y from x.
Keeps the equality specified by the left set.

Visibility: export
symDifference : ListSetv->ListSetv->ListSetv
  Set symmetric difference. Uses the union of the differences.

Visibility: export
intersection : ListSetv->ListSetv->ListSetv
  Set intersection. Implemented as the difference of the union and the symetric difference.

Visibility: export
toSortedSet : Ordv=>ListSetv->SortedSetv
Visibility: public export