search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

`unfold id n` tactic #119

Open lambdacalculator opened 5 years ago

lambdacalculator commented 5 years ago

Given that one of the possible witnesses is unfold(id,n,witness1,...,witnessn) (where the second n should really be k), wouldn't it make sense to have a tactic unfold id n, so that it wouldn't be necessary to litter one's specifications with names just so that specification clauses could be unfolded? I've often wished I had this ability when a search doesn't succeed: it would allow me to work backwards to find where the search is failing without having to redo my specification by adding names to all the clauses that might be involved.

chaudhuri commented 5 years ago

Seems reasonable. Thanks for the suggestion. I'll take a crack at it RSN.