issues
search
uwplse
/
PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
MIT License
51
stars
2
forks
source link
Decompiler Test Suite
#74
Open
randair
opened
4 years ago
randair
commented
4 years ago
Decompiler needs lots of regression tests. Plan:
.v full of terms
decompile command to print decompiled tactics to console
ground truth file to diff with
Decompiler needs lots of regression tests. Plan: