reorderForall

Mathlib.Tactic.ToAdditive.Frontend

URI: https://scilib.ai/kg/mathlib#ToAdditive.reorderForall

Lean4

/-- Reorder pi-binders. See doc of `reorderAttr` for the interpretation of the argument -/
def reorderForall (reorder : List (List Nat)) (src : Expr) : MetaM Expr := do
  if let some maxReorder := reorder.flatten.max? then
    forallBoundedTelescope src (some (maxReorder + 1)) fun xs e => do
        if xs.size = maxReorder + 1 then
          mkForallFVars (xs.permute! reorder) e
        else
          throwError "the permutation\n{reorder}\nprovided by the `(reorder := ...)` option is \
                        out of bounds, the type{(indentExpr src)}\nhas only {xs.size} arguments"
  else
    return src

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

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

Разделы

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

Аффилиация

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