Proof: Difference between revisions

Content added Content deleted
Line 290: Line 290:
addition {j, i} ())
addition {j, i} ())


(* 3.4 Try to prove that sum of two evens is odd. *)
(* 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 ===