iterateExactly'

Mathlib.Tactic.Core

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

Lean4

/-- `iterateExactly' n t` executes `t` `n` times. If any iteration fails, the whole tactic fails.
-/
def iterateExactly' : Nat → m Unit → m Unit
  | 0, _ => pure ()
  | n + 1, tac => tac *> iterateExactly' n tac

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

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

Разделы

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

Аффилиация

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