Convert function on Fin n to list

Stream: new members

[Vivek Rajesh Joshi]

Is there a method to convert a function f : Fin n -> A to a list with elements of type A, containing the outputs of the function?

[Eric Wieser]

Have you tried asking loogle?

[Eric Wieser]

@loogle Fin n → A, List A

[loogle]

:exclamation: unknown identifier 'n'
Did you mean Fin Fin.Value.n → A, List A, Fin BitVec.Literal.n → A, List A, or something else?

[Eric Wieser]

@loogle Fin ?n → A, List A

[loogle]

:exclamation: unknown identifier 'A'
Did you mean Fin ?n → GeneralizedContinuedFraction.Pair.a, List A, Fin ?n → Cubic.a, List A, or something else?

[Eric Wieser]

@loogle Fin ?n → ?A, List ?A

[loogle]

:search: List.get, List.sizeOf_get, and 125 more

[Eric Wieser]

@loogle (Fin n → A) → List A

[loogle]

:exclamation: unknown identifier 'n'
Did you mean (Fin Fin.Value.n → A) → List A, (Fin BitVec.Literal.n → A) → List A, or something else?

[Eric Wieser]

@loogle (Fin ?n → ?A) → List ?A

[loogle]

:search: List.ofFn, List.ofFnTR, and 3 more

[Eric Wieser]

Hopefully that also shows you how to refine your loogle query!

[Eric Wieser]

(docs#List.ofFn is the answer you want)

[Vivek Rajesh Joshi]

Thanks! Got more than I expected out of this thread :smiley: