и встал на скользкую дорожку инфиксного использования S-комбинатора

Читая в прошедшем семестре курс матлогики, придумывал разные задачки для практики и многие решал (для себя) на Агде. Сейчас сел все это упорядочивать. Обнаружил, что сопоставление с образцом, конечно же, обыгрывает явные элиминаторы по выразительности при записи доказательств, но элиминаторы иногда сопротивляются довольно успешно. ( Read more... )