module difflist.

kind dlist     type -> type.

type   minus   list A -> list A -> dlist A.
infixr minus   5.

type concat    dlist A -> dlist A -> dlist A -> o.

concat (L minus K) (K minus M) (L minus M).

type d_palindrome   dlist A -> o.

d_palindrome (L minus L).
d_palindrome ((X::L) minus L).
d_palindrome ((X::L) minus K) :- d_palindrome (L minus (X::K)).

type make_dlist   list A -> dlist A -> o.

make_dlist nil (M minus M).
make_dlist (X::L) ((X::K) minus M) :- make_dlist L (K minus M).

type make_list   dlist A -> list A -> o.

make_list (L minus nil) L.