The Coq mailing list

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

Here it is

Require Import List.
Require Import Le.
Require Import Compare_dec.

Definition hd (A:Set) (l : list A) :=
   match l return (length l > 0 -> A) with
   | nil    => fun H : length nil > 0 => False_rec A (le_Sn_O 0 H)
   | a :: _ => fun _ => a
   end.


Definition f (l2: list nat) : option nat.
intros l2.
refine(
  if zerop (length l2) then None else
  Some (hd nat l2 _)
  );
auto.
Defined.