Дал клоду 3.7 (со всеми этими дипсинками и формал-режимом) простую задачку, уровень лабы первого курса (в плане программирования конечно) -- сделать простенькие анимации для Окружности в HoTT: базовая точка, которая может образовывать Петли (просто бегает по кругу), и элементарная деформация (демонстрация гомотопической эквивалентности).

В конструктивном смысле это отправная точка для рекурсивных определений функций (из высших индуктивных типов в другие типы), что скоро будем изучать ))))

3.7 зафигачил 100 строк: сперва вроде работает, но когда переключаешься по кнопочкам разных анимаций, визуализация сбивается. Я ему пару раз подсказал "как должно работать", он вполне ожидаемо стал вносить локальные приляпки, из-за чего возможность какого-то дальнейшего расширения скрипта быстро сошла на нет.