# Executable Specification

[View higher-order.sig]
[View higher-order.mod]
sig higher-order.
kind a, alist type.
type anil alist.
type acons a -> alist -> alist.
type mappred (a -> a -> o) -> alist -> alist -> o.
type swap (a -> a -> o) -> (a -> a -> o).
type star (a -> a -> o) -> (a -> a -> o).
type and o -> o -> o.
type exist (a -> o) -> o.

module higher-order.
exist P :- P X.
and P Q :- P, Q.
mappred P anil anil.
mappred P (acons X XS) (acons Y YS) :- P X Y, mappred P XS YS.
swap P X Y :- P Y X.
star P X X.
star P X Y :- P X Z, star P Z Y.