You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
Given that one of the possible witnesses is
unfold(id,n,witness1,...,witnessn)
(where the second
n
should really bek
), wouldn't it make sense to have a tacticunfold 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 asearch
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.The text was updated successfully, but these errors were encountered: