There are many tactics in the standard library, such as the simpl_list
, simpl_map
, etc. which do not have a in
form. This is awkward, because many a times, I'd like to run simpl_list
within the context of a hypothesis.
Is there some way to enable this?
For your specific example, simpl_list
is just autorewrite with list
so you can do autorewrite with list in H
. I don't see simpl_map
in the standard library.
Unfortunately there's no general way to take a tactic and run it in another context (specifically, the in H
, in *
, and in *|-
variants the builtin tactics tend to provide). It's also a fairly manual process to write each of these variants and use Tactic Notation
to give the same syntax, which is why you don't always see all the variants.