# Sets¶

Sets provide an alternate representation of logical operators.

## Syntax¶

syntax setexpr
{
cmp := "in"
cmp := "\in"
cmp := "\notin"
cmp := "\owns" ;

x[ssetunion_pri] := x[ssetunion_pri] "\cup" x[>ssetunion_pri]
x[ssetintersection_pri] := x[ssetintersection_pri] "\cap" x[>ssetintersection_pri]
}


## Semantics¶

class Set[c,t] {
fun mem (elt:t, container:c):bool => elt \in container;
virtual fun \in : t * c-> bool;
fun \owns (container:c, elt:t) => elt \in container;
fun \ni (container:c, elt:t) => elt \in container;
fun \notin (elt:t, container:c) => not (elt \in container);

fun \cup[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e \in x or e \in y }
;

fun \cap[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e \in x and e \in y }
;

fun \setminus[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e \in x and e \notin y }
;
}


A set is any type with a membership predicate $$\in$$ spelled \in. You can also use function mem. The parser also maps in to operator \in.

We also provide a reversed form :math::owns spelled \owns, and negated forms $$\ni$$ spelled ni or notin.

Three combinators are provided as well, $$\cap$$ spelled \cap provides intersection, $$\cup$$ spelled \cup provides the usual set union, and $$\setminus$$ spelled setminus the asymmetic set difference or subtraction.

Note that sets are not necessarily finite.