[Coq-Club] weird idtac

[Erkki Luuk]

Hi

Can someone please explain this:

Require Import Ensembles.
Variable (n:nat) (r:Set).
Parameter natt:> nat -> Type.
Notation "{ x , y }" := ltac:(tryif first [refine (In Type (Couple Type x
y) _)
| exact (In Type (Couple Type x y) y)]
then idtac "ok" else idtac "{..,..} fail"; fail) (at level 9).
Notation "' x" := ltac:(first [refine (Couple_l Type (natt x) r)
| refine (Couple_r Type n x)]) (at level 9).
Check 'n: {n,r}. (*ok. Error: Tactic failure*)

It's strange enough to get "ok. Error: Tactic failure" here, *but* if I
comment "idtac "{..,..} fail";" out, I get "ok" and everything works.
Tested on 8.8.1

Cheers
Erkki

[Bagnall, Alexander]

I'm no ltac expert, but it looks like it may due to the low parsing precedence of ';'.

In general (e.g., in OCaml),
if a then b else c; d
parses as:
(if a then b else c); d
If you want:
if a then b else (c; d)
then you must include the parentheses.

- Alex B
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Erkki Luuk <***@gmail.com>
Sent: Tuesday, September 18, 2018 3:02:22 PM
To: coq-***@inria.fr
Subject: [Coq-Club] weird idtac

Hi

Can someone please explain this:

Require Import Ensembles.
Variable (n:nat) (r:Set).
Parameter natt:> nat -> Type.
Notation "{ x , y }" := ltac:(tryif first [refine (In Type (Couple Type x y) _)
| exact (In Type (Couple Type x y) y)]
then idtac "ok" else idtac "{..,..} fail"; fail) (at level 9).
Notation "' x" := ltac:(first [refine (Couple_l Type (natt x) r)
| refine (Couple_r Type n x)]) (at level 9).
Check 'n: {n,r}. (*ok. Error: Tactic failure*)

It's strange enough to get "ok. Error: Tactic failure" here, *but* if I comment "idtac "{..,..} fail";" out, I get "ok" and everything works. Tested on 8.8.1

Cheers
Erkki

[Erkki Luuk]

Indeed, thanks
Erkki

Post by Bagnall, Alexander
I'm no ltac expert, but it looks like it may due to the low parsing precedence of ';'.
In general (e.g., in OCaml),
if a then b else c; d
(if a then b else c); d
if a then b else (c; d)
then you must include the parentheses.
- Alex B
------------------------------
*Sent:* Tuesday, September 18, 2018 3:02:22 PM
*Subject:* [Coq-Club] weird idtac
Hi
Require Import Ensembles.
Variable (n:nat) (r:Set).
Parameter natt:> nat -> Type.
Notation "{ x , y }" := ltac:(tryif first [refine (In Type (Couple Type x y) _)
| exact (In Type (Couple Type x y) y)]
then idtac "ok" else idtac "{..,..} fail"; fail) (at level 9).
Notation "' x" := ltac:(first [refine (Couple_l Type (natt x) r)
| refine (Couple_r Type n x)]) (at level 9).
Check 'n: {n,r}. (*ok. Error: Tactic failure*)
It's strange enough to get "ok. Error: Tactic failure" here, *but* if I
comment "idtac "{..,..} fail";" out, I get "ok" and everything works.
Tested on 8.8.1
Cheers
Erkki