The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Hi Adam,
>
> It actually isn't idiomatic to program with subset types in Coq! I
> recommend avoiding explicit dependently typed programming whenever
> possible.  There should be a high standard of justification for any
> explicit dependent types (which are sometimes the right tool for a
> job).  It tends to be painful to define and reason about such
> programs.  Experts generally avoid it.
>
thanks for your advice. I actually guessed that much by now. However, my
intention here was to experience and understand the nature of the pain :)

Klaus