The Coq mailing list

[Erkki Luuk <erkkil AT gmail.com>]

Indeed, thanks

Erkki

On Tue, Sep 18, 2018 at 10:40 PM, Bagnall, Alexander <ab667712 AT ohio.edu> wrote:

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-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Erkki Luuk <erkkil AT gmail.com>
Sent: Tuesday, September 18, 2018 3:02:22 PM
To: coq-club AT 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