Stack

A stack is simply a list with two operations:

private
  data Stack (A : Type) : Type where
    []   : Stack A
    _::_ : A → Stack A → Stack A
 
pop : {A : Type} → Stack A → Maybe (A × Stack A)
pop []       = nothing
pop (x :: xs) = just (x , xs)
 
push : {A : Type} (x : A) (xs : Stack A) -> Stack A
push x xs = _::_