First you cannot imagine have a hd
function from list A
to A
for an arbitrary A
. This is why you need a default
argument in the definition of hd
. This leads to hd : A -> list A -> A
.
Then in your code for maphd
, the term hd a
should be hd default a : A
for some appropriate default
element of type A
. So the most direct modification of your maphd
would be:
Fixpoint maphd (default : A) (l: list (list A)) : (list A):=
match l with
| nil => nil
| a :: t => (hd default a):: (maphd default t)
end.
which leads to maphd default [ [] ] = [ default ]
.
Now if you want maphd
to throw away empty lists, you have to say so in the code:
Fixpoint maphd (l: list (list A)) : (list A):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t => (hd a (a::r)):: (maphd t)
end.
(here choosing a
as default
argument) but then the call to hd
can be inlined to get:
Fixpoint maphd (l: list (list A)) : (list A):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t => a :: (maphd t)
end.