The Coq mailing list

[jean-francois.monin AT imag.fr]

You're right, I meant:

Definition lift_T : Set :=
  match a with None => option empty | Some a' => option (B a') end.

Thanks,
  JF

roconnor AT theorem.ca
 a ecrit :
 > On Mon, 23 Jan 2006 
 > jean-francois.monin AT imag.fr
 >  wrote:
 > 
 > > Matter of taste, since option empty is isomorphic to unit.
 > > One may prefer to return option something in all cases.
 > 
 > Ah.  You omitted `option' and just wrote `empty' in your mail, so the code
 > didn't work for me.
 > 
 > -- 
 > Russell O'Connor                                      <http://r6.ca/>
 > ``All talk about `theft,''' the general counsel of the American Graphophone
 > Company wrote, ``is the merest claptrap, for there exists no property in
 > ideas musical, literary or artistic, except as defined by statute.''
 > 
 >