Mathlib Map

Theorems · Definition · category theory

TypeVec.append1

{n : ℕ} → TypeVec.{u_1} n → Type u_1 → TypeVec.{u_1} (n + 1)

Support for extending a TypeVec by one element.

Defined in
Mathlib.Data.TypeVec
Cited by
67 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TypeVec.appendFun · cited by 42TypeVec.appendFunMvQPF.Cofix.dest · cited by 13Cofix.destMvPFunctor.M.dest · cited by 12M.destMvPFunctor.appendContents · cited by 10MvPFunctor.appendContentsTypeVec.RelLast' · cited by 8TypeVec.RelLast'MvQPF.Fix.mk · cited by 7Fix.mkMvPFunctor.wDest' · cited by 7MvPFunctor.wDest'TypeVec.appendFun_comp · cited by 6TypeVec.appendFun_compTypeVec.appendFun_comp_id · cited by 5TypeVec.appendFun_comp_idTypeVec.appendFun_comp_splitFun · cited by 5TypeVec.appendFun_comp_sp…TypeVec.appendFun_id_id · cited by 5TypeVec.appendFun_id_idMvQPF.recF · cited by 5MvQPF.recFMvQPF.Cofix.corec · cited by 5Cofix.corecMvPFunctor.wMk' · cited by 5MvPFunctor.wMk'MvQPF.Cofix.dest_corec · cited by 4Cofix.dest_corecTypeVec · cited by 185TypeVecFin2 · cited by 145Fin2TypeVec.append1CITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • TypeVecstatement and proof · cited by 185
  • Fin2proof · cited by 145

Cited by102

Results whose statement or proof uses this declaration.