The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 08/18/2015 10:50 PM, Vadim Zaliva wrote:
> Are there are other, alternative representations for such functions? My 
> current one works but
> proofs look a big messy as expressions end up littered with projection 
> function applications.
For exactly that reason I tend to prefer total (non-dependently typed) 
functions most of the time. In that case, you could just return a dummy 
value if the input is outside of the domain. Separately from that, you 
could prove that the result of the function is within its range, 
provided the input is within the domain.