mkRecNames

Mathlib.Util.CompileInductive

URI: https://scilib.ai/kg/mathlib#Mathlib.Util.mkRecNames

Lean4

/-- Returns the names of the recursors for a nested or mutual inductive,
using the `all` and `numMotives` arguments from `RecursorVal`. -/
def mkRecNames (all : List Name) (numMotives : Nat) : List Name :=
  if numMotives ≤ all.length then all.map mkRecName
  else
    let main := all[0]!
    all.map mkRecName ++ (List.range (numMotives - all.length)).map (fun i => main.str s! "rec_{i + 1}")

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

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

Разделы

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

Аффилиация

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