Proof: Difference between revisions
→{{header|ATS}}
Line 224:
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.
Another thing to note is that ATS contains multiple sublanguages, and that proofs are ''not'' done in the same sublanguage as executable code. There are dependent types of a practical kind, but not at all in the way some other languages have dependent types as first-class objects of the full language.
| |||