canonical way to build `Fin 3 -> a`?

Stream: Is there code for X?

[Siddharth Bhat]

Given three values x, y, z : a, what's the canonical way to build a function f : Fin 3 -> a such that f 0 = x, f 1 = y, and f 2 = z? Bonus points if the answer generalizes to all n :)

[Mario Carneiro]

![x, y, z]

[Siddharth Bhat]

Thanks! For future reference, how could I have found that out for myself?

[Mario Carneiro]

which desugars to uses of Fin.cons

[Mario Carneiro]

Siddharth Bhat said:

Thanks! For future reference, how could I have found that out for myself?

Ask about it on #Is there code for X?