An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
refactoring dependent-types coq transport repair coq-plugin ornaments devoid pumpkin-patch proof-reuse algebraic-ornaments proof-repair equivalences pumpkin-pi proof-refactoring proof-assistants
-
Updated
Sep 18, 2024 - Coq