The Coq mailing list

["Zhaozhong Ni" <nzz AT acm.org>]

I think the following works:

Definition F (A B : Set) (x : A) (y : R(A->B)) : R(B) :=
 match y with
   Rep y0 => Rep B (y0 x)
 end.

-Zhaozhong

----- Original Message ----- 
From: "Zhong Shao" <shao AT cs.yale.edu>
To: 
<coq-club AT pauillac.inria.fr>
Cc: 
<flint-core AT cs.yale.edu>
Sent: Thursday, February 03, 2005 2:44 PM
Subject: [Flint-core] Dependent elimination question? 


> Hi, given the following induction definition: 
>
>   Inductive R (A : Set) : Type := 
>        Rep : A -> R(A).
>
> assume that Set is a predicative universe (as in Coq 8.0),
>
> Can I write a function F with the following type: 
>
>            (forall A B : Set) A -> R(A -> B) -> R(B)
>
> The naive way is to write it as: 
>
>  Definition F (A B : Set) (x : A) (y : R(A->B)) : R(B) := 
>     match y with 
>       Rep y0 => Rep (y0 x)
>     end.
>
> which of course does not work since y0 does not has type A->B.
>
> Thanks a lot,
>
> -Zhong Shao
> (shao-zhong AT cs.yale.edu)
> _______________________________________________
> Flint-core mailing list
> Flint-core AT cs.yale.edu
> http://netra.cs.yale.edu/mailman/listinfo/flint-core