The Coq mailing list

[jean-francois.monin AT imag.fr]

You can.

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

Inductive empty := Set :.

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

Definition lift : lift_T.
unfold lift_T; case a.
  intros a'; exact (Some (f a')).
  exact None.
Defined.


Fabrice Lemercier a ecrit :
 > Does it mean that I cannot generalize my lifting
 > function to dependent types?
 > 
 > --- 
 >Â roconnor AT theorem.ca
 >  a écrit :

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 44