toExpr — Mathlib

English

There is a canonical ToExpr instance for Fin n → α, allowing evaluation of such functions into expressions.

Русский

Существует каноничный экземпляр ToExpr для Fin n → α, позволяющий представлять такие функции в выражениях.

LaTeX

$$$[ToExpr]\, (\mathrm{Fin} \ n \to \alpha)$$$$

Lean4

protected instance _root_.PiFin.toExpr [ToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α) :=
  have lu := toLevel.{u}
  have eα : Q(Type $lu) := toTypeExpr α
  let toTypeExpr := q(Fin $n → $eα)
  { toTypeExpr, toExpr v := PiFin.mkLiteralQ fun i => show Q($eα) from toExpr (v i) }

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