The inverse of list.ofFn

Stream: Is there code for X?

[Hyeokjun Kwon]

Is there an inverse of list.ofFn?
I am aware that if I have a list, I can do ![...] to make a function so I was hoping there might be something with type similar to List A → ( (Fin (l.length)) → A ) which would do the same thing but for a list in the proof.

[Floris van Doorn]

This is docs#List.get

[Joachim Breitner]

@loogle |- List ?a -> Fin _ -> ?a
is disappointing. It's something with patterns with a plain metavariable at the conclusion that Loogle just doesn't like .

[loogle]

:shrug: nothing found

[Yury G. Kudryashov]

@loogle List, Fin

[Joachim Breitner]

@loogle List, Fin

[loogle]

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