view final_pre/src/AgdaSingleLinkedStack.agda @ 7:28f900230c26

add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents
children c8bfe73b2faf
line wrap: on
line source

-- Implementation
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}


popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack stack cs with (top stack)
...                                | Nothing = cs stack  Nothing
...                                | Just d  = cs stack1 (Just data1)
  where
    data1  = datum d
    stack1 = record { top = (next d) }