English
PiFin.mkLiteralQ constructs a quasi-quoted finite function notation from a family of quasi-quoted α indexed by Fin n.
Русский
PiFin.mkLiteralQ формирует квазицитируемое обозначение конечной функции из семейства квазицитируемых α, индексируемого Fin n.
LaTeX
$$$\PiFin.mkLiteralQ : (\mathrm{Fin}\ n \to Q(\alpha)) \to Q(\mathrm{Fin}\ n \to \alpha)$$$
Lean4
/-- `mkVecLiteralQ ![x, y, z]` produces the term `q(![$x, $y, $z])`. -/
def _root_.PiFin.mkLiteralQ {u : Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q($α)) : Q(Fin $n → $α) :=
loop 0 q(vecEmpty)
where/-- The core logic of `loop` is that `loop 0 ![] = ![a 0, a 1, a 2] = loop 1 ![a 2]`, where
recursion starts from the end. In this example, on the right-hand side, the variable `rest := 1`
tracks the length of the current generated notation `![a 2]`, and the last used index is
`n - rest` (`= 3 - 1 = 2`). -/
loop (i : ℕ) (rest : Q(Fin $i → $α)) : Q(Fin $n → $α) :=
if h : i < n then loop (i + 1) q(vecCons $(elems (Fin.rev ⟨i, h⟩)) $rest) else rest
