%%% syntax for the dequeue problem
%%%
%%% #load "dequeue_syntax.mod".
%%% #query dequeue_syntax.

module dequeue_syntax. % syntax for doubly ended queues

kind deq		type -> type.

% dequeue terms
type emptydeq		deq T.
type deq_precat		deq T -> T -> deq T.
type deq_postcat	deq T -> T -> deq T.

% deq observers
type deq_has		deq T -> T -> o.
type deq_size		deq T -> int -> o.
type deq_head		deq T -> T -> o.
type deq_last		deq T -> T -> o.
type deq_init		deq T -> deq T -> o.
type deq_tail		deq T -> deq T -> o.
type deq_count		deq T -> T -> int -> o.
type deq_isEmpty	deq T -> o.
type deq_equal		deq T -> deq T -> o.