I’m trying to define a Fixpoint
function for list X
to get its first half of sub-list, if it’s odd number of elements then the middle element doesn’t count in.
Here’s what I’ve tried:
<code>Fixpoint half {X : Type} (l : list X) : list X :=
match l with
| [] => []
| h :: t => match (rev t) with
| [] => []
| p :: b => [h] ++ (half (rev b))
end
end.
</code>
<code>Fixpoint half {X : Type} (l : list X) : list X :=
match l with
| [] => []
| h :: t => match (rev t) with
| [] => []
| p :: b => [h] ++ (half (rev b))
end
end.
</code>
Fixpoint half {X : Type} (l : list X) : list X :=
match l with
| [] => []
| h :: t => match (rev t) with
| [] => []
| p :: b => [h] ++ (half (rev b))
end
end.
Yet it gives error:
Cannot guess decreasing argument of fix.
What am I missing here?