The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Sun, Jul 14, 2013 at 6:54 PM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr>
 wrote:

> For efficiency reasons, I would personally favor the
>
> T + { a = remove }

I have two questions about this idiom:

(1)  In what sense is it more efficient?
(2)  If I know that (a <> remove), how do I extract a return value of
type T? It's probably simple, but I've so far been unable to do this.

> idiom. Actually, if you plan on writing programs rather than proofs, I would
> even get rid of the dependency and write it in two parts, as a partial
> function and a specification lemma :

Ah, indeed. I understand the alternatives you suggest. In this case,
however, my work is more about proofs than programs. The programs I'm
writing are only examples.

Thanks!

--
www.mhelvens.net