Мягкое введение в Coq: используем тактики

[DZhon]

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

[Shekeen]

А можете добавить в каждую статью цикла ссылки на другие части? Хочется потом сесть и сразу все прочитать и попробовать, ссылки бы сильно упростили процесс перехода на следующие части.

[ymn]

Готово.

[Shekeen]

Спасибо!

[Brotherofken]

Да, содержание очень поможет, ведь не меньше сотни «статей» наберётся, если писать по 1-2 страницы печатного текста за раз.