Most of the ATS examples begin with something which looks like ML, but as the types are made more and more strict they end up looking like incredibly verbose C.
To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous.
For example:
Definition Prime p := forall n m, n * m = p -> n = 1 \/ m = 1.
All of these variables have type nat, which Coq can infer from the use of "*" and "=".
To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous.
For example:
All of these variables have type nat, which Coq can infer from the use of "*" and "=".