Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | new work on elimination tactic | Josh Chen | 2020-05-24 | 1 | -15/+23 |
* | some tweaks and comments, in preparation for general inductive type elimination | Josh Chen | 2020-05-22 | 1 | -0/+5 |
* | Brand-spanking new version using Spartan infrastructure | Josh Chen | 2020-04-02 | 1 | -0/+33 |