mkProdSplitElem

Mathlib.Tactic.FunProp.ToBatteries

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

Lean4

/-- For an element of a product type(of size`n`) `xs` create an array of all possible projections
i.e. `#[xs.1, xs.2.1, xs.2.2.1, ..., xs.2..2]` -/
def mkProdSplitElem (xs : Expr) (n : Nat) : MetaM (Array Expr) :=
  (Array.range n) |>.mapM (fun i ↦ mkProdProj xs i n)

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

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

Разделы

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

Аффилиация

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