The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/28/2012 03:27 PM, Bingzhou wrote:
> So, I think the first step is to define predicates or relations such as
> emptydomain, subsetOfDomain, continuous and bounded ...
>    

Perhaps you are assuming that functions in Coq are partial by default?  
In fact, the function space of [->] is total: every element of the type 
on the left is mapped to exactly one element of the type on the right.  
The standard approach to encoding a partial function from [A] to [B] is 
to use [A -> option B].  With such a representation, it makes sense to 
start talking about the domains of functions, in a way that allows you 
to discuss, for instance, values that are not in the domain.