Hi, is there a way to match on shelved goals using Ltac?
You have the Unshelve command (to unshelve everything), the unshelve tactical (to use when creating shelved goals to unshelve them), shelve and shelve_unifiable to undo unshelve.
And often shelved goals are really evars that can be recognized by using is_evar on the goal.
TLDR: not AFAIK but there's lots that might help for many use cases
Sorry, I think I wasn't specific enough about my issue. I have an Ltac that should do an
autorewrite with some_db where the lemmas in
some_db create a bunch of shelved goals then I'd like to run an Ltac on these shelved goals.
So intuitively what I though of doing
Ltac bar := ... Ltac foo := autorewrite with some_db; Unshelve; try bar.
Unshelve is not available within Ltac and using
unshelve (try bar) also does not work
you probably want to do
unshelve (autorewrite with some_db); try bar.
Thanks! I misunderstood what unshelve does!
As a follow up: If I generalize my tactic to
Ltac foo tac := unshelve (ltac:(tac)); try bar; shelve_unifiable.
Doesn't work when using
foo (autorewrite with some_db) because it seems to not bracket properly (this also happens when I don't wrap tac as an ltac)
Maybe the following would help?
Tactic Notation "foo" tactic3(tac) := unshelve tac; try bar; shelve_unifiable.
I never remember where arguments are thunked or not in Ltac.
Thank you @Rodolphe Lepigre ! This works as intended
Last updated: Oct 04 2023 at 23:01 UTC