Proof: Difference between revisions
Content added Content deleted
Line 290: | Line 290: | ||
addition {j, i} ()) |
addition {j, i} ()) |
||
(* 3.4 Try to prove |
(* 3.4 Try to prove the sum of two evens is odd. *) |
||
#if 0 (* Change to 1 to see the attempted proof rejected. *) |
#if 0 (* Change to 1 to see the attempted proof rejected. *) |
||
Line 333: | Line 333: | ||
<pre>$ patscc proof-primitively.dats && ./a.out |
<pre>$ patscc proof-primitively.dats && ./a.out |
||
Success!</pre> |
Success!</pre> |
||
=== A more usual use of ATS === |
=== A more usual use of ATS === |