%%% syntax for finite sets
%%%
%%% #load "set_syntax.mod".
%%% #query set_syntax.

module set_syntax.  % types for homogeneous finite sets.

kind set		type -> type.

% set terms
type emptyset		set T.
type set_insert		set T -> T -> set T.

% set observers
type has		set T -> T -> o.
type set_delete		set T -> T -> set T -> o.
type set_union		set T -> set T -> set T -> o.
type set_intersect	set T -> set T -> set T -> o.
type set_size		set T -> int -> o.
type subseteq		set T -> set T -> o.
type set_equal		set T -> set T -> o.