Unable to use List.map with List.get

Stream: new members

[Vivek Rajesh Joshi]

I have a nested list and I want to turn it into a list of functions on Fin. I'm trying to use List.get, but it isn't working. How do I fix this?

variable (M : Matrix (Fin r) (Fin s) Rat)
def rowListofMat := List.map List.ofFn (List.ofFn M)
example : ∀ i, ((rowListofMat M).get i).length = r := by
  intro i
  let p := List.map (List.get (α:=Rat)) (rowListofMat M) --application type mismatch

[Matt Diamond]

I think the problem is that List.map doesn't take a dependent function, which is what you're giving it when you pass in List.get.

[Matt Diamond]

you could use List.getD with a fallback value (e.g. List.getD (α := Rat) (fallback := 0))

that works because then you're passing in a function of type List α → ℕ → ℚ

you could also use List.get? (α:=Rat) and get a function of type List α → ℕ → Option ℚ

the point is to remove the dependency on the length of the list

[Matt Diamond]

you're asking for a list of functions on Fin, but you're forgetting that Fin isn't a type, it's a type constructor... the type is Fin n for some value of n

[Matt Diamond]

I suppose you could also define def mapList (l : List α) : (n : ℕ) × (Fin n → α) := ⟨l.length, l.get⟩ and then use that with List.map to get a List ((n : ℕ) × (Fin n → ℚ)) but I have no idea if that would be useful to you