module stack where

pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
pushSingleLinkedStack stack data next = next stack1
  where
    element = record {next = top stack; data = data}
    stack1  = record {top = just element}


popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
popSingleLinkedStack stack data next with (top stack) =
  ... | nothing = next stack nothing
  ... | just a  = next stack1 data1
    where
      data1 = data a
      stack1 = record { top = (next a)}