Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] making a proof done with assert transparent

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] making a proof done with assert transparent


Chronological Thread 
  • 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/



Archive powered by MHonArc 2.6.18.

Top of Page