Proof: Difference between revisions
Content added Content deleted
Line 219: | Line 219: | ||
=={{header|ATS}}== |
=={{header|ATS}}== |
||
Although probably I could do more precisely what is asked, and encode some formal logic in the ATS proofs language, that is not what I do below. Rosetta Code is here to show what a language can do, and so it seems better to show a bit of how ATS ''actually'' would be used. |
|||
In that case, addition is a poor operation upon which to base the demonstration. ''Multiplication'' would be much better, because ATS has relatively little built-in knowledge of multiplication; the operation has to be defined by axioms or recursively from addition. But I shall stick with addition, just the same. |
|||
<lang ATS>(* ATS does not contain a full-fledged proof language, but does |
<lang ATS>(* ATS does not contain a full-fledged proof language, but does |
||
Line 327: | Line 333: | ||
<pre>$ patscc proof.dats && ./a.out |
<pre>$ patscc proof.dats && ./a.out |
||
Success!</pre> |
Success!</pre> |
||
=={{header|Coq}}== |
=={{header|Coq}}== |