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