Execute tactic block n times

Stream: new members

[Donald Sebastian Leung]

In Coq, we can execute a tactic or sequence of tactics n times by do n some_tactic or do n (tactic1; tactic2; ...; tactic_n). Is there a similar functionality in Lean?

[Johan Commelin]

iterate n { foo, bar }

[Donald Sebastian Leung]

Thanks!