Theory Stack_Aux

theory Stack_Aux
imports Stack
begin

text‹The function ‹list› appends the two lists and is needed for the list abstraction of the deque.›

fun list :: "'a stack ⇒ 'a list" where
  "list (Stack left right) = left @ right"

instantiation stack ::(type) size
begin

fun size_stack :: "'a stack ⇒ nat" where
  "size (Stack left right) = length left + length right"

instance..
end

end