История изменений
Исправление buddhist, (текущая версия) :
По поводу того, как это делают в Идрисе: http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf
В ATS вообще не считается зазорным использовать другой стиль.
// ТС, твоей проблеме соответствует листинг №8 в файле по ссылке
Исходная версия buddhist, :
По поводу того, как это делают в Идрисе: http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf
В ATS вообще не считается зазорным использовать другой стиль.