loc.wildcard

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

should loc.wildcard include the current goal as well? That is, if I want to apply a tactic at *, I should get both local_context and target, right?

Is there a single command that returns local_context ++ target?
EDIT: This part is somewhat nonsense, since, even though local_context appears to have type list expr and target appears to have type expr, I think that local_context are the names of the variables in the context, while target is the type of the goal.

The question of whether tactic at * should mean all hypotheses and also the target still holds!

Thanks!

[Mario Carneiro]

yes, at * means all hypotheses and the target

[Mario Carneiro]

src#interactive.loc.apply contains the reasoning about this case. You should usually use this instead of destructuring loc directly

[Damiano Testa]

Ah, i did not know. I did something, maybe I'll have to change it a little bit.