Zulip Chat Archive

Stream: general

Topic: At hypothesis


view this post on Zulip 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 ...
  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.

view this post on Zulip 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: May 13 2021 at 22:15 UTC