Revising the ATS code for arrays, simplifying the specification so I can add in what I have from the smt file.