strings of fixed length

Stream: new members

[Bjørn Kjos-Hanssen]

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]

vector is what you are looking for

[Bjørn Kjos-Hanssen]

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]

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]

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?

[Yury G. Kudryashov]

Yes, it is true.

[Yury G. Kudryashov]

See docs#fin.ext

[Yury G. Kudryashov]

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

[Bjørn Kjos-Hanssen]

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

[Yury G. Kudryashov]

docs#propext

[Bjørn Kjos-Hanssen]

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

[Kenny Lau]

you can use subtypes

[Bjørn Kjos-Hanssen]

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

[Yury G. Kudryashov]

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