iterateRange

Mathlib.Tactic.Core

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

Lean4

/-- `iterateRange m n t`: Repeat the given tactic at least `m` times and
at most `n` times or until `t` fails. Fails if `t` does not run at least `m` times.
-/
def iterateRange : Nat → Nat → m Unit → m Unit
  | 0, 0, _ => pure ()
  | 0, b, tac => iterateAtMost b tac
  | (a + 1), n, tac => do
    tac;
    iterateRange a (n - 1) tac

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

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

Разделы

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

Аффилиация

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