## Stream: general

### Topic: hlist

#### Scott Morrison (Sep 15 2018 at 07:05):

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

#### Kenny Lau (Sep 15 2018 at 07:06):

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

#### Scott Morrison (Sep 15 2018 at 07:07):

I want to be able to specify the types:

#### Scott Morrison (Sep 15 2018 at 07:07):

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

#### Scott Morrison (Sep 15 2018 at 07:08):

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

#### Chris Hughes (Sep 15 2018 at 07:19):

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

#### Kenny Lau (Sep 15 2018 at 07:20):

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

#### Keeley Hoek (Sep 15 2018 at 07:31):

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

#### Scott Morrison (Sep 15 2018 at 07:45):

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

#### Scott Morrison (Sep 15 2018 at 07:46):

(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 (Sep 15 2018 at 07:51):

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

#### Scott Morrison (Sep 15 2018 at 07:51):

but this isn't exhaustive

#### Mario Carneiro (Sep 15 2018 at 08:02):

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

#### Mario Carneiro (Sep 15 2018 at 08:13):

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

#### Mario Carneiro (Sep 15 2018 at 08:14):

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

Last updated: Aug 03 2023 at 10:10 UTC