add 'notypeclasses apply' tactic
notypeclasses apply
is like notypeclasses refine
except that it adds sufficiently many underscores automatically, thus making it less fragile to use.
This version adds underscores until the term is not a function any more. That is less smart than apply
/apply:
, so maybe we should pick a different name? We could also try applying after each _
, though that could be slow if unification goes wrong.
@msammler I found a case in the bitvector lib that seems like it could use the new tactic. I hope it is covered by tests, otherwise I am not sure if it still works.^^
Fixes #220 (closed)
Merge request reports
Activity
This version adds underscores until the term is not a function any more. That is less smart than
apply
/apply:
, so maybe we should pick a different name? We could also try applying after each_
, though that could be slow if unification goes wrong.That behavior does not seem too great, and indeed makes it quite different from
apply
/apply:
. It makes it especially awkward sincerefine
does not respect transparency at all, so if the definition internally contains an arrow/forall,_
s will be applied for those.That said, I do not have a clear vision of the potential use cases of this tactic. I guess it will mostly be a building block for other tactics, so perhaps it's OK to fix this problem later when it shows up in practice.
- Resolved by Robbert Krebbers
It makes it especially awkward since
refine
does not respect transparency at all, so if the definition internally contains an arrow/forall,_
s will be applied for those.No that does not follow. We use
opose_specialize_foralls_core
to determine how many_
to add, which IIRC is entirely syntactic and does not unfold anything.That said, I do not have a clear vision of the potential use cases of this tactic. I guess it will mostly be a building block for other tactics, so perhaps it's OK to fix this problem later when it shows up in practice.
My current vision is "replace all the
notypeclasses refine
with long sequences of_
in the Iris Proof Mode".added S-waiting-for-review label
- Resolved by Ralf Jung
removed S-waiting-for-review label
added 9 commits
-
35ad6bee...e3a6f3ef - 8 commits from branch
master
- 6d672976 - add 'notypeclasses apply' tactic
-
35ad6bee...e3a6f3ef - 8 commits from branch
added S-waiting-for-review label
removed S-waiting-for-review label
mentioned in commit ada66bd2