добавлял в pattern-match catch-all условие в конце, которое возвращало бы мэтч неизменённым?
Вот для этого и хотелось бы какой-то макрос, чтобы каждый раз не писать так х)
Конкретно так не знаю, чтобы реализовывали. В Coq в OCaml API есть "map_with_binders", используемый для обхода дерева выражений. Рекурсивный вызов его самого не изменяет дерева, зато можно делать точечные изменения по месту. https://coq.github.io/doc/v8.11/api/coq/EConstr/index.html#iterators
Обсуждают сегодня