The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

This is sort of a follow-up from the previous thread on safe-head.
Suppose I want to define a function

Definition safe_head (A:Set) (l:list A) (pf: l <> nil) : A.

I can start with

intro A.
refine(fun (l:list A) (pf: l <> nil)  => match l with
  | nil => _
  | cons x xs => _
  end). 

That gives me two goals

2 subgoals
A : Set
l : list A
pf : l <> nil
______________________________________(1/2)
A


______________________________________(2/2)
A

But I can no longer see that in the first goal l = nil, and in the second goal
l = cons x xs. What am I doing wrong?

Thanks,

Edsko