list of length n from `fin n -> X`

Stream: general

[Kevin Buzzard]

I have f : fin n -> X and I want [f(0),f(1),...f(n-1)]. I could list.map if I had the list [0 : fin n, 1 : fin n, ...]. I could use list.pmap assuming I can find a proof that s \in range(n) -> s < n. Is there an idiomatic way to do this?

[Marc Huisinga]

https://github.com/leanprover-community/mathlib/blob/02659d634db53d4fc58a76d219402fbbaaa2b51f/src/data/list/defs.lean#L337 ?

[Kevin Buzzard]

Thanks! I'm not sure I was even aware of that file!

[Marc Huisinga]

there's also https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/init/data/list/basic.lean for list defs from core

[Kevin Buzzard]

I want (of_fn {n} f).length = n. I'll prove it myself I guess.

[Kevin Buzzard]

oh there's a huge section on it in data.list.basic

[Marc Huisinga]

indeed!

[Kevin Buzzard]

oh wow data.list.basic imports data.list.defs! I had always assumed that basic was the first one, as a general rule.

[Floris van Doorn]

Usually basic is indeed the most basic file in a folder.
In this case, mathlib tactics want to use definitions on lists, and basic properties about list want to use mathlib tactics, which (probably) caused list definitions to be separated out from list.basic.