The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On 15 Apr 2009, at 11:35, Matej Kosik wrote:

> 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.

Edsko