## Stream: new members

### Topic: strings of fixed length

#### Bjørn Kjos-Hanssen (Dec 14 2020 at 20:34):

I can represent the set of all binary strings of length 3 as the type (fin 3) \to (fin 2). Is there a way to associate that type with lists [0,0,0], [0,0,1], ...? Or in other words, instead of writing list (fin 2) is there something like list_of_length 3 (fin 2)?

#### Johan Commelin (Dec 14 2020 at 20:35):

vector is what you are looking for

#### Bjørn Kjos-Hanssen (Dec 14 2020 at 20:43):

Great... and then access values of f: vector (fin 2) 3 by f.nth 0, f.nth 1, f.nth 2 it seems

#### Yury G. Kudryashov (Dec 15 2020 at 03:14):

See also docs#vector.of_fn for the other direction. I don't know if there is an equiv with docs#vector.of_fn and docs#vector.nth as to_fun and inv_fun.

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 04:27):

I seem to drift towards accessing entries of f using the complicated expressions (f.nth 0).val, (f.nth 1).val, (f.nth 2).val. :thinking: Because I don't know if it's true that m.val = n.val → m = n for m n : fin 2?

Yes, it is true.

See docs#fin.ext

#### Yury G. Kudryashov (Dec 15 2020 at 04:32):

In Lean any two proofs of the same proposition are equal.

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 04:34):

Awesome, so there's no "Hott" :grin:

docs#propext

#### Bjørn Kjos-Hanssen (Dec 16 2020 at 05:50):

How about binary strings of length at most 3? Any easy way to turn that into a type?

#### Kenny Lau (Dec 16 2020 at 06:45):

you can use subtypes

#### Bjørn Kjos-Hanssen (Dec 16 2020 at 06:53):

Thanks yes it's time for some reading :book:

#### Yury G. Kudryashov (Dec 17 2020 at 17:29):

{l : list (fin 2) // length l ≤ 3}

Last updated: May 15 2021 at 22:14 UTC