equal
deleted
inserted
replaced
115 |
115 |
116 |
116 |
117 \section{An Introductory Proof} |
117 \section{An Introductory Proof} |
118 \label{sec:intro-proof} |
118 \label{sec:intro-proof} |
119 |
119 |
120 Assuming you have input the declarations and definitions of \texttt{ToyList} |
120 Assuming you have processed the declarations and definitions of |
121 presented so far, we are ready to prove a few simple theorems. This will |
121 \texttt{ToyList} presented so far, we are ready to prove a few simple |
122 illustrate not just the basic proof commands but also the typical proof |
122 theorems. This will illustrate not just the basic proof commands but |
123 process. |
123 also the typical proof process. |
124 |
124 |
125 \subsubsection*{Main Goal.} |
125 \subsubsection*{Main Goal.} |
126 |
126 |
127 Our goal is to show that reversing a list twice produces the original |
127 Our goal is to show that reversing a list twice produces the original |
128 list. |
128 list. |