The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Benjamin Werner wrote:
> Hi,
>
> >  Correspondingly, there's no way you can construct a predicate
> > P on functions such that P f is inhabited and P g is empty when f and g
> > agree on all arguments: the only thing P can do with its function is
> > apply it.
>
> Actually you can construct such a predicate. You will be able to exhibit 
> a proof of P f. It will also be true that there is no closed proof of P 
> g. 
>
> If I am too obscure here, I can try to elaborate when I have a little 
> more time.

Point taken. (f =) is such a P, of course.

Perhaps I meant to say 'P f is inhabited and P g is Empty'.

Cheers

Conor

--
http://www.cs.nott.ac.uk/~ctm