Мягкое введение в Coq: индуктивные определения

[dima_mendeleev]

Я думаю стоит написать как с (S (S O)) получаются циферки.

[dima_mendeleev]

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