Try tactic

Stream: lean4

[Marcus Rossel]

I feel like I've seen this before, but I'm not sure how to search for it:
Is there some way to try a tactic and if it fails run a different tactic instead?
Something like (pseudo code):

example : ... := by
  ...
  try (rw [h]) else (rw [←h])

[Tomas Skrivan]

The try tactic is defined here https://github.com/leanprover/lean4/blob/3be437cad378e848da063ef16e67b8eca7ff73c0/src/Init/Tactics.lean#L141 you separate different tactics by | e.g. try (rfl | simp)

[Tomas Skrivan]

Hmm the example might be wrong, I'm on phone and can't test it now.

[Lars König]

try is defined using first, so you can also use that. first tries the given tactics until the first one succeeds.

first
| rw [h]
| rw [←h]
| ...