pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} !$\rightarrow$! SingleLinkedStack Data !$\rightarrow$! Data !$\rightarrow$! (Code : SingleLinkedStack Data !$\rightarrow$! t) !$\rightarrow$! t
pushSingleLinkedStack stack datum next = next stack1
  where
    element = cons datum (top stack)
    stack1  = record {top = Just element}

-- Basic stack implementations are specifications of a Stack

singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} !$\rightarrow$! StackMethods {n} {m} a {t} (SingleLinkedStack a)
singleLinkedStackSpec = record {
                           push = pushSingleLinkedStack
                         ; pop  = popSingleLinkedStack
                         }

createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} !$\rightarrow$! Stack {n} {m} a {t} (SingleLinkedStack a)
createSingleLinkedStack = record {
                        stack = emptySingleLinkedStack ;
                        tackMethods = singleLinkedStackSpec
                        }