Information lost during conversion of List Fin to nestedlist

Stream: new members

[Vivek Rajesh Joshi]

I have a function that converts a list of functions on Fin r to a list of lists. How do I ensure that the information about the length of the function being r is not lost during conversion? More specifically, how do I prove the example below?

def rowListAux : List (Fin r → Rat) → List (List Rat)
| [] => []
| a::as => [List.ofFn a] ++ (rowListAux as)

example (f : List (Fin r → Rat)) : ∀ i, ((rowListAux f).get i).length = r := by sorry

[Eric Wieser]

Your function can be written more succinctly as List.map List.ofFn

[Eric Wieser]

Which will then make the example much easier to prove, because there are lots of lemmas about map

[Vivek Rajesh Joshi]

Thanks, that does make my functions simpler