Агата Сомова · старший инспектор
Тимофей Ильич третий день считает обложки в папках. Сколько в папке всего, как глубоко лежит самый дальний лист, какие простейшие листы встречаются. Хватит. Сегодня отдел пишет свою первую программу. Костя, не бледней: язык называется Haskell, и он устроен так же, как правила со стены.
Костя никогда не программировал. Ты, может быть, тоже. Это не помеха: программа будет короткой, а каждая её строка повторяет то, что ты уже знаешь о термах из урока 28.
Главная мысль урока такая. Термы собраны по правилам, поэтому и функции над ними, и доказательства о них идут по тем же правилам: по случаю на каждый вид терма, с опорой на части. Для функций это называют структурной рекурсией, для доказательств структурной индукцией.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.