The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

> Definition take : forall (x:list nat) (n:nat), list nat.
> intros.
> induction n.

This is wrong, you should generalize x, since it is going to vary
in the recursive call.

An undocumented feature to define recursive function in proof mode
is fix. It takes as parameter the ranks o the structural argument.
On your function:

Definition take : forall (x:list nat) (n:nat), list nat.
fix 2.
intros l [| n].
exact (@nil nat).
destruct l as [|h t].
exact (@nil nat).
exact (h::take t n).
Defined.

The nice thing is now that
  Print take.
gives you the expected code

--
Laurent