Zulip Chat Archive

Stream: general

Topic: At hypothesis

Sorawee Porncharoenwase (Nov 21 2020 at 08:59):

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 ...

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 (Nov 21 2020 at 12:38):

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.

Last updated: Dec 20 2023 at 11:08 UTC