search

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
MIT License
51 stars 2 forks source link

Decompile coq terms into tactic list. #71

Closed randair closed 4 years ago

randair commented 4 years ago

intro/intros tactics. ./build.sh && ./test.sh