The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

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