hlist

Stream: general

[Scott Morrison]

Does anyone know if we have heterogenous lists (hlist) somewhere in mathlib?

[Kenny Lau]

is that just list Σ T : Type u, T?

[Scott Morrison]

I want to be able to specify the types:

[Scott Morrison]

so if I have T : list (Type u), I want hlist T

[Scott Morrison]

with length the same at T, and the i-th element has type the i-th element of T.

[Chris Hughes]

{L : list (Σ T : Type u, T) // L.map sigma.fst =T}

[Kenny Lau]

what are the lemmas that you want to prove regarding hlist?

[Keeley Hoek]

I've definitely seen them somewhere.... sorry

[Scott Morrison]

Ugh, what's the trick for matching on fin n?

[Scott Morrison]

(Thanks, Chris, for your suggestion. I agree that would have worked; but I decided to just use dependent functions on fin n for now.)

[Scott Morrison]

I've got a n : fin 2 and want to write match n with | \< 0, _ \> := ... | \<1, _\> := ... end

[Scott Morrison]

but this isn't exhaustive

[Kenny Lau]

how about fin.succ_rec_on

[Mario Carneiro]

I certainly have a definition of hlist sitting around somewhere, but I never managed to get it mathlib ready

[Mario Carneiro]

I pushed to a hlist branch on community mathlib: https://github.com/leanprover/mathlib/commit/b5d6d6

[Mario Carneiro]

I want to be clear that I'm not really advocating this representation, this is more of an experiment. It also doesn't completely compile since the top half of the file was rewritten more than the bottom