The Coq mailing list

[jean-francois.monin AT imag.fr]

Matter of taste, since option empty is isomorphic to unit.
One may prefer to return option something in all cases.

  JF

roconnor AT theorem.ca
 a ecrit :
 > On Mon, 23 Jan 2006 
 > jean-francois.monin AT imag.fr
 >  wrote:
 > 
 > > You can.
 > 
 > I think you mean to say:
 > 
 > Section Foo.
 > 
 > Variable (A:Set)(B:A->Set)(f:forall a, B
 > a)(a:option A).
 > 
 > Definition lift_T : Set :=
 >   match a with None => unit | Some a' => option (B a') end.
 > 
 > Definition lift : lift_T.
 > unfold lift_T; case a.
 >   intros a'; exact (Some (f a')).
 >   constructor.
 > Defined.
 > 
 > End Foo.
 > 
 > Check lift.
 > 
 > lift
 >      : forall (A : Set) (B : A -> Set),
 >        (forall a : A, B a) -> forall a : option A, lift_T A B a
 > 
 > 
 > -- 
 > 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.''
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
 > 
 >