freshName

Mathlib.Tactic.ITauto

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ITauto.freshName

Lean4

/-- Get a new name in the pattern `h0, h1, h2, ...` -/
@[inline]
def freshName : StateM Nat Name := fun n => (Name.mkSimple s! "h{n}", n + 1)

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

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

Разделы

Аффилиация

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