Данная статья является переводом моей статьи: Formalization of code in Coq - tactics , написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола...

Предисловие Сопоставление с образцом в Coq на первый взгляд выглядит не сложнее, чем в большинстве языков программирования, т.е. довольно просто. Правда, это впечатление остаётся только до тех пор,...