pragma SPARK_Mode (On);

with Stacks;
function Main return Integer
is
	package Integer_Stacks is new Stacks(Integer,0);
	use Integer_Stacks;
	S: Stack;
begin
	Empty(S);
	Push(S,2); --Push(S,3);
	Pop(S);
	--if Size(S) > 0 then
		return Top(S);
	--else
	--	return 0;
	--end if;
end Main;