coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] weird idtac

From: Erkki Luuk <erkkil AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] weird idtac
Date: Tue, 18 Sep 2018 22:02:22 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=erkkil AT gmail.com; spf=Pass smtp.mailfrom=erkkil AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
Ironport-phdr: 9a23:XUN84hYa8pjptSK80YMxkgL/LSx+4OfEezUN459isYplN5qZocq7bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoyyb5EMD+oCPOZTso/zp0YTrRu9GAKhA/3gyiVLhn/13K061/8sEQ7D3AM6HtIOtG7Yo8nyNKcXSO24yrTDwzbbb/5Oxzvx9IzFfgoirPyMR758bMvcxEg1Gw7KgFidr5HuMSmP2eQXqWeb6vJtVeKxhG4jrAF8uj2vyd0tionNn44Vy1fE+ThgzIY7KtC1RlR3YdGjEJtXuCGaM5V5Ttk+TGFvvSY20rwGuZilcygW0Jkr2QLTZvidf4WL4h/vTvudLDZ5iX5/d7+yiQ6+8U26xe39Usm03kxKri1AktTUqH8NzR/T6suGSvt55Uqh1jOP2BrS6uFAO0w7ia3bK5s5zr4qipUTqVjDHjPxmEjukKCWcVwk9vG05OTjf7XpvYSRN5R0iwH7KqQhgNazAeU+MggUXmiU4/6w1LP5/R6xfLIfhfov16LdrZryJMIBp6f/DRUG/Jwk7kOSFTSl0Zw8gGQEZAZIYhGEjozBNFTHIfS+BvC61Qf/2Ax3zuzLa+WySq7GKWLOxe+4LORNrnVEwQ929uhxopddC7UPOvX2Axaju9nRDxt/OAuxkb++VIdNk7gGUGfKOZe3dbvIuAbRtO0qKuiIIoQSvWSlcqV317vVlXY83GQlU+yp0J8QMi3qG/1nJwCYZiOpjItaV2gNuQU6Qarhj1jQCTM=

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

[Coq-Club] weird idtac, Erkki Luuk, 09/18/2018
- Re: [Coq-Club] weird idtac, Bagnall, Alexander, 09/18/2018
  - Re: [Coq-Club] weird idtac, Erkki Luuk, 09/18/2018