The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 23 Jan 2006, Fabrice Lemercier wrote:

> Does it mean that I cannot generalize my lifting
> function to dependent types?

I suggest returning option {a0 : A &  B a0}:

Section Foo.

Variable (A:Set)(B:A->Set)(f:forall a, B
a)(a:option A).

Definition lift : option {a:A & (B a)} :=
 match a with
   None => None
 | Some a' => Some (existS (fun x => B x) a' (f a'))
 end.

End Foo.

Check lift.

lift
     : forall (A : Set) (B : A -> Set),
       (forall a : A, B a) -> option A -> option {a0 : A &  B a0}


-- 
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.''