HOrElse for lists

Stream: Is there code for X?

[Moritz Doll]

Does this exist somewhere already? Probably way more general, since only the HOrElse class is used

def foo (goal : MVarId) (tacs : List (MVarId → MetaM Unit)) : MetaM Unit :=
  match tacs with
  | [] => pure ()
  | f :: fs => f goal <|> (foo goal fs)

I want to chain together 'finishing' tactics (aka functions MVarId → MetaM Unit), which should be a rather common thing to do.

[Eric Wieser]

docs#list.mfirst is almost that in Lean3. docs4#List.mfirst maybe?

[Eric Wieser]

Are you sure you don't want your base case to be failure?

[Moritz Doll]

ah, yes it should be failure

[Moritz Doll]

the lean4 version of list.mfirst is docs4#List.firstM