Мягкое введение в Coq: индуктивные определения
В предыдущей части мы научились задавать новые типы и строить функции над их значениями. В этой небольшой заметке я более подробно остановлюсь на индуктивных определениях, чтобы внести ясность и наметить дальнейшие темы для изучения. Ранее я сказал, что в Coq нет батареек. На самом деле я слукавил — в Coq есть стандартная библиотека, которая содержит множество полезных определений. Помимо стандартной библиотеки существуют и более специфические вещи, на которых мы пока не будем останавливаться.Читать дальше →
