(*
 *     THE STACK DATATYPE (THE SPECIFICATION)
 *
 *)

data S -> stack(A) = push: S -> SF(A) => S
                   | pop : S -> S * SF(A).


(* AN IMPLEMENTATION: *)

def a_stack: 1  -> stack(A)

           = () => (| l => push: ff   => []
                               | ss a => cons (a, l)

                    |      pop: { []           => ([], ff)
                                | cons (a, l') => (l', ss a)
                                }
                                  l
                    |)
                       [].