mkProdProj

Mathlib.Tactic.FunProp.ToBatteries

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

Lean4

/-- For `(x₀, .., xₙ₋₁)` return `xᵢ` but as a product projection.

We need to know the total size of the product to be considered.

For example for `xyz : X × Y × Z`
  - `mkProdProj xyz 1 3` returns `xyz.snd.fst`.
  - `mkProdProj xyz 1 2` returns `xyz.snd`.
-/
def mkProdProj (x : Expr) (i : Nat) (n : Nat) : MetaM Expr := do
  -- let X ← inferType x
    -- if X.isAppOfArity ``Prod 2 then

  match i, n with
  | _, 0 =>
    pure x
  | _, 1 =>
    pure x
  | 0, _ =>
    mkAppM ``Prod.fst #[x]
  | i' + 1, n' + 1 =>
    mkProdProj (← withTransparency .all <| mkAppM ``Prod.snd #[x]) i' n'

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

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

Разделы

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

Аффилиация

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