iterateAtMost

Mathlib.Tactic.Core

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Tactic.iterateAtMost

Lean4

/-- Repeats a tactic at most `n` times, stopping sooner if the
tactic fails. Always succeeds. -/
def iterateAtMost : Nat → m Unit → m Unit
  | 0, _ => pure ()
  | n + 1, tac =>
    try
      tac;
      iterateAtMost n tac
    catch _ =>
      pure ()

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru