At hypothesis

Stream: general

[Sorawee Porncharoenwase]

I wonder if it's possible to create a tactic at_hyp so that every tactic inside its block acts on the given hypothesis. E.g.,

at_hyp h {
  rewrite ...
  simp ...
  rewrite ...
  unfold_coe
}

would be equivalent to:

  rewrite ... at h
  simp ... at h
  rewrite ... at h
  unfold_coe at h

This would be easy if we can create new tactics like rewrite_h, simp_h, unfold_coe_h, etc. to cooperate with at_hyp. But can we do it without creating new tactics? In particular, every parse location will automatically receive h.

[Alex J. Best]

You can do conv at h {} already to get rewrite, simp, ring and some others. I'm not sure about unfold_coes, perhaps that feature needs adding to conv.