Induction - Githubissues

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

MIT License

51 stars 2 forks source link

Induction #79

Closed randair closed 4 years ago

randair commented 4 years ago

Induction for simple motives and naively placed simpls.
zoom_lambda_names and fresh_name might want to be in coq-plugin-lib?
fun_args record, also put somewhere in coq-plugin-lib?

randair commented 4 years ago

Thanks for taking a look! I'm wondering if regression tests for induction should be saved until we know exactly what the output should look like? For example, this commit doesn't have bulleting, which I can add next commit, but also where simpl. should go. I could add tests for examples which definitely don't require simpl.?

tlringer commented 4 years ago

I would add tests that work for now and tweak them when we change the format. And I would add some tests that currently fail, but write that they should fail and in the testing script, expect them to fail. That way, when they stop failing, you'll know you have succeeded at the next steps.