List of Fin n from list of natural numbers

Stream: Is there code for X?

[Hannah Fechtner]

Hi all - I have a list a of natural numbers, and I know it is bounded above by some constant n. I want to convert this to a list of Fin n. I have as a hypothesis

h :  ∀ (x : ℕ), x ∈ a → x < n

I want to do something like

List.map (λ i => Fin.mk i _) a

Where the underscore is, I need to apply h and the fact that x ∈ a ... which is only true because we're mapping the function onto a.

Is there a neat way to do this?

My other thought was to use option types and clean the final list later, but that feels so gross

[Ruben Van de Velde]

docs#List.attach is the general approach here

[Hannah Fechtner]

For anyone looking at this later, List.attach works fine, but List.pmap is easier to use induction with :)