section ‹Idle›
theory Idle
imports Stack
begin
text ‹Represents the `idle' state of one deque end.
contains a ‹stack› and its size as a natural number.›
datatype (plugins del: size) 'a idle = Idle "'a stack" nat
fun push :: "'a → 'a idle → 'a idle" where
"push x (Idle stack stackSize) = Idle (Stack.push x stack) (Suc stackSize)"
fun pop :: "'a idle → ('a * 'a idle)" where
"pop (Idle stack stackSize) = (Stack.first stack, Idle (Stack.pop stack) (stackSize - 1))"
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
¤
*© Formatika GbR, Deutschland
