Комментарии 4
Для начинающегося кокера это выглядит очень загадочно. Было бы лучше:
1) Если был бы дистиллированный пример с теоремой и большим количеством однотипных конструкторов.
2) Если было бы очевидно, в каком из 4х вариантов тактики destr_if прячутся все эти однотипные 12 вариантов. Я предполагаю, что в последнем, но совсем не уверен.
Спасибо за комментарий. Я тоже думала про дистиллированные примеры, с ними много возни, больше времени придется потратить (чем брать, что есть), но это сделает качественней статью, это точно.
Я уж и сама не помню, где там в destr_if прячутся однотипные варианты, это нужно разбираться, отрывать код.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Формальная верификация кода на Coq: тактики