Proof: Difference between revisions
→An unusual use of ATS
Line 225:
Nevertheless, one can see that ATS is capable of some "abstract" reasoning. In fact, the prelude includes a recursive definition of multiplication, and in the [[Greatest_common_divisor#ATS|ATS entry for the greatest common divisor task]] I present ''practical'' (not "first principles") definitions of the gcd both by way of axioms and by recursive prop.
And the following does show, by total functions, how to construct a particular number (by counting up to it) and how to add (again by counting). That proofs of such things as "evens add up to evens" are then trivialized is perhaps a point ''in favor of'' ATS, ''as a systems programming language''.
| |||