Здравствуйте, Ziaw, Вы писали:

Z>Аналогия не верна. ПМ используется во всех проектах и используется очень широко. Логический решатель — узкая ниша.

Я же смайл поставил.

А если по делу, мне крайне не нравится реализация алгебраических типов в Немерле. Она там одинакова для рекурсивных и нерекурсивных АглТД, т.е. явно была сделано "на скорую руку". Но нынешняя команда сим вопросом заниматься не будет.