Repeating until nothing changes

Stream: new members

[Guilherme Espada]

Is there a way to repeat a tactic until nothing changes in the context? I guess somewhat similar to simp, but with a custom list of tactics

[Horatiu Cheval]

Is docs#repeat what you're looking for?
It takes a tactic (or a succession of tactics) as argument

[Guilherme Espada]

What I tried before posting was something along the lines of:

repeat{
 try{
  b
 },
 try{
  b
 },
}

However, this doesn't quite work: it seems to run until failure. The tries are needed because if you have multiple possible options, I don't want one fail to prevent the other from running (at an unspecified order). In fact, a tactic may fail in one cycle and work in the next.

[Guilherme Espada]

Unless there is a tactic that takes n subtactics and succeeds if any succeed, that would work

[Yakov Pechersky]

try { a <|> b <|> c} for the latter idea

[Guilherme Espada]

Thanks! Works like a charm!

[Scott Morrison]

You might also like src#tactic.chain (but probably too specialized for its application in tactic#tidy for others to use).