coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How is exactly_once supposed to work?

From: Jonathan <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] How is exactly_once supposed to work?
Date: Wed, 25 Jun 2014 20:47:34 -0400

From the documentation, I would have thought the following would fail:

Section X.
Variable n : nat.
Variable m : nat.
Goal nat.
Proof.
exactly_once assumption.
Qed.
End X.

If this is supposed to succeed, then what is meant by "at most one success" in the documentation for exactly_once?

-- Jonathan

[Coq-Club] How is exactly_once supposed to work?, Jonathan, 06/26/2014
- Re: [Coq-Club] How is exactly_once supposed to work?, Arnaud Spiwack, 06/26/2014