mkUncurryFun

Mathlib.Tactic.FunProp.ToBatteries

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.mkUncurryFun

Lean4

/-- Uncurry function `f` in `n` arguments. -/
def mkUncurryFun (n : Nat) (f : Expr) : MetaM Expr := do
  if n ≤ 1 then
    return f
  forallBoundedTelescope (← inferType f) n fun xs _ ↦ do
      let xProdName : String ←
        xs.foldlM (init := "") fun n x ↦ do
            return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes)
      let xProdType ← inferType (← mkProdElem xs)
      withLocalDecl (.mkSimple xProdName) default xProdType fun xProd ↦ do
          let xs' ← mkProdSplitElem xProd n
          mkLambdaFVars #[xProd] (← mkAppM' f xs').headBeta

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

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

Разделы

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

Аффилиация

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