The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Edsko de Vries a écrit :
> > or perhaps the special case were
> > `a' does not occur free in `B':
> >
> >        E,Γ |- A:Prop      E,Γ |- B:Set
> >        ----------------------------------
> >            E,Γ |- A->B:Set
> >
> > Is it possible to give some meaningful examples of terms that can be
> > constructed this way?
>
> Such functions are valid only in special cases; in particular, it is 
> possible to use a proof as argument to a function that returns an 
> argument in Set if the proof is used *only* to guard termination of the 
> function, but cannot otherwise influence the value returned. If you are 
> working through Coq'Art, you'll get to such functions eventually: 
> Sections 14.2.3 and 15.2.

Could someone give bibliographic references about this limitation?