The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Patricia, you just have to tell coq to make A and B
implicit parameters of the constructor lambda1. Here
is how to do it:

========

Inductive Pi (A:Set)(B:A->Set):Set:=
| lambda1 (b:forall (x:A),B x) : Pi A B.

Implicit Arguments lambda1 [A B].

Definition Arrow (A:Set)(B:Set):Set :=
Pi A (fun x:A => B).

Definition isArrow (A:Set)(B:Set)(b:A->B) : Arrow A B := lambda1 b.

========

Cheers,

--
gallais


On 31 October 2012 21:19, Patricia Peratto 
<psperatto AT adinet.com.uy>
 wrote:
> I have defined as inductive sets in the way of Martin-Lof
> universal quantification:
>
> Inductive Pi (A:Set)(B:A->Set):Set:=
> | lambda1 (b:forall (x:A),B x) : Pi A B.
> I have defined the arrow set as a particular case of
> the Pi set:
>
> Definition Arrow (A:Set)(B:Set):Set :=
> Pi A (fun x:A => B).
> I want to define elements in the arrow set using the
> constructor of the Pi set.
>
> I have done the definition that is shown below, but
> does not work.
>
> Definition isArrow (A:Set)(B:Set)(b:A->B):
> Arrow A B := lambda1 (fun (x:A)=> b x).
>
> Someone knows why?
>
> Regards
>
> Patricia