\begin{patch}{ExitXmpPagePatch1} \begin{paste}{ExitXmpPageFull1}{ExitXmpPageEmpty1} \pastebutton{ExitXmpPageFull1}{\hidepaste} \tab{5}\spadcommand{n := 0\bound{n }} \indentrel{3}\begin{verbatim} (1) 0 Type: NonNegativeInteger \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty1} \begin{paste}{ExitXmpPageEmpty1}{ExitXmpPagePatch1} \pastebutton{ExitXmpPageEmpty1}{\showpaste} \tab{5}\spadcommand{n := 0\bound{n }} \end{paste}\end{patch} \begin{patch}{ExitXmpPagePatch2} \begin{paste}{ExitXmpPageFull2}{ExitXmpPageEmpty2} \pastebutton{ExitXmpPageFull2}{\hidepaste} \tab{5}\spadcommand{gasp(): Exit == free n n := n + 1 error "Oh no!" \bound{gasp }\free{n }} \indentrel{3}\begin{verbatim} Type: Void \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty2} \begin{paste}{ExitXmpPageEmpty2}{ExitXmpPagePatch2} \pastebutton{ExitXmpPageEmpty2}{\showpaste} \tab{5}\spadcommand{gasp(): Exit == free n n := n + 1 error "Oh no!" \bound{gasp }\free{n }} \end{paste}\end{patch} \begin{patch}{ExitXmpPagePatch3} \begin{paste}{ExitXmpPageFull3}{ExitXmpPageEmpty3} \pastebutton{ExitXmpPageFull3}{\hidepaste} \tab{5}\spadcommand{half(k) == if odd? k then gasp() else k quo 2 \bound{half }\free{gasp }} \indentrel{3}\begin{verbatim} Type: Void \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty3} \begin{paste}{ExitXmpPageEmpty3}{ExitXmpPagePatch3} \pastebutton{ExitXmpPageEmpty3}{\showpaste} \tab{5}\spadcommand{half(k) == if odd? k then gasp() else k quo 2 \bound{half }\free{gasp }} \end{paste}\end{patch} \begin{patch}{ExitXmpPagePatch4} \begin{paste}{ExitXmpPageFull4}{ExitXmpPageEmpty4} \pastebutton{ExitXmpPageFull4}{\hidepaste} \tab{5}\spadcommand{half 4\free{half }\bound{app1 }} \indentrel{3}\begin{verbatim} (4) 2 Type: PositiveInteger \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty4} \begin{paste}{ExitXmpPageEmpty4}{ExitXmpPagePatch4} \pastebutton{ExitXmpPageEmpty4}{\showpaste} \tab{5}\spadcommand{half 4\free{half }\bound{app1 }} \end{paste}\end{patch} \begin{patch}{ExitXmpPagePatch5} \begin{paste}{ExitXmpPageFull5}{ExitXmpPageEmpty5} \pastebutton{ExitXmpPageFull5}{\hidepaste} \tab{5}\spadcommand{half 3\free{half app1 }\bound{app2 }} \indentrel{3}\begin{verbatim} \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty5} \begin{paste}{ExitXmpPageEmpty5}{ExitXmpPagePatch5} \pastebutton{ExitXmpPageEmpty5}{\showpaste} \tab{5}\spadcommand{half 3\free{half app1 }\bound{app2 }} \end{paste}\end{patch} \begin{patch}{ExitXmpPagePatch6} \begin{paste}{ExitXmpPageFull6}{ExitXmpPageEmpty6} \pastebutton{ExitXmpPageFull6}{\hidepaste} \tab{5}\spadcommand{n\free{app2 }} \indentrel{3}\begin{verbatim} (5) 1 Type: NonNegativeInteger \end{verbatim} \indentrel{-3}\end{paste}\end{patch} \begin{patch}{ExitXmpPageEmpty6} \begin{paste}{ExitXmpPageEmpty6}{ExitXmpPagePatch6} \pastebutton{ExitXmpPageEmpty6}{\showpaste} \tab{5}\spadcommand{n\free{app2 }} \end{paste}\end{patch}