Dependent lists/vectors in Mathlib

Stream: new members

[Mathias Stout]

Are there any good examples in the Mathlib on how to best deal with dependent lists/vectors with a given 'signature'?

Essentially, I mean an object of the following type,

def DepListAsFun {S : Type*} (σ : List S) (α : S → Type*)  := (i : Fin (σ.length)) → (α σ[i])

an object of this type could equivalently be represented by a structure like

structure DepList {S : Type*} (σ : List S) (α : S → Type*) where
  toList : List (Sigma α)
  proj_eq : toList.map (Sigma.fst) = σ

or many other different types.

I am particularly interested in operations like appending, mapping, casting over equality of signature σ, and converting between different avatars, but don't want to reinvent the wheel if possible.

(My specific context is formalizing tuples of variables in many-sorted first order logic, but I imagine that such objects pop up elsewhere as well.)

[Aaron Liu]

docs#List.TProd

[Aaron Liu]

is what I've been using

[Mathias Stout]

Oh that seems interesting, thanks for directing me to it.
Do you happen to know if it has been used beyond Measure theory or if there are further lemmas/definitions converting between different presentations of this kind of object beyond what is listed on the docs page for TProd?

[Aaron Liu]

I know it isn't supported very well and people have been telling me to use something else instead

[Mathias Stout]

Oh, ok, I see. Thanks!