coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] making a proof done with assert transparent
- Date: Tue, 13 Oct 2015 05:58:21 +0200
Hi
On Mon, Oct 12, 2015 at 12:11:47PM -0400, Jason Gross wrote:
> As suggested in the bug report, you can try something like:
>
> Tactic Notation "transparent" "assert" "(" ident(H) ":" uconstr(type) ")" :=
> refine (let H := (_ : type) in _).
This is cool, but there is still a little detail. I take an example
in my code. It was initially
assert (Saxy : (a = x) * (a = y) → isSet (x = y)).
But, if I add "transparent"
transparent assert (Saxy : (a = x) * (a = y) → isSet (x = y)).
The "*" is highlighted and I get the message
Toplevel input, characters 35-36:
Syntax error: ')' expected after [tactic:uconstr] (in
[tactic:simple_tactic]).
Same error message if I define "transparent assert" with "constr" or
with "open_constr" instead of "uconstr".
To make it work, I must put the type between parentheses
transparent assert (Saxy : ((a = x) * (a = y) → isSet (x = y))).
In the simple assert version these parentheses are not required.
--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/
- [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
- RE: [Coq-Club] making a proof done with assert transparent, Soegtrop, Michael, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Jason Gross, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Jason Gross, 10/12/2015
- RE: [Coq-Club] making a proof done with assert transparent, Soegtrop, Michael, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Ilmārs Cīrulis, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
Archive powered by MHonArc 2.6.18.