Hi! I am very new to Coq and I’m trying to prove a simple matrix transpose function. As part of my matrix transpose, I have a function called
maphd, which takes the head of each item in a list of lists, and returns the result as a new list.
Fixpoint maphd (l: list (list A)): (list A):= match l with | nil => nil | a :: t => (hd a):: (maphd t) end.
However, this fails with the error:
In environment A : Type maphd : list (list A) -> list A l : list (list A) a : list A t : list (list A) The term "maphd t" has type "list A" while it is expected to have type "list (list (list A) -> list A)".
I don’t know how to put this right!