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

[@dima_mendeleev]

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

[@dima_mendeleev]

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