coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Overloading the forall notation
- Date: Tue, 21 Apr 2020 23:32:54 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f44.google.com
- Ironport-phdr: 9a23:dE4CthMAtsgeqpCIZsUl6mtUPXoX/o7sNwtQ0KIMzox0Iv7/rarrMEGX3/hxlliBBdydt6sZzbaI+P6wEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe9bL9oIxi7rArdu8gVjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVQTlgzkbOTEn7G7Xi9RwjKNFrxKnuxx/2JPfbIWMOPZjYq/RYdYWSGxGUchMSixBGZu8YJUTAOodM+hYqIz9qEEPrRu4GAKgAOzixztNinLwwKY00fkuERve0QMvH9wAvnfaosjrOqgOSu261rXEwC/ZYv9KxTvw6o7FeQ0hr/GWWrJwdNLcx0g1FwzbgVWQrpblPjOI3eoKqWeb6/RvWv6vi2E9tgp8pTevxsI2hYnNmI0a1lDE+j9izYY6IN23Uk97Ydq+HJRMsCGaMpJ7T8U/SG9mvyY6z6cJuZ+9fCUSx5QnxgLfa/yac4eT+B7jVeGRLDFlj3xmYLKynwi+/VSkx+HmVcS50ExGojdbntTPrHwA2BPe586aQfVn5EihwyyA1wXL5+FEP080ka3bJoYkwrEql5oTtV3PHyHzmEnrlaOWeEop9+ey5+ToZbXmoZCcN4tqhQ3kLqsuncm/Dfw5MggIQWeb5fyx2KP/8UD9WrlHjf07nrPEvJzEJskXvKG0DgBN3oYm8Rm/DjOm0NoCnXkAKVJIYB2Hj43zNFHKPv/3Efe/jE63nTdkwvDJJLzhApHXInffl7fheK5x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK0O4OempnskkxdJdq6wmJATdXqQH/J8Ikzfb2C60fkbFmJfkRAzQ+vwmRWnWDpebHa7F/Yz4zg/BYmmBK/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZLX/Le5Mzonk/TbGkDrQZ+1S2rgajkuhoK+PV/msTspexjIEotd2Wrgk78HlPN+rY02yJSDspzGYBRjtzw6Um5EIhlhGM1q93h/EeHttWtasQA1UKcKXExuk/MOjcHwfIf9OHUlGjG4z0DjQ4T9Z3yNgLMR9w
Hello --
--
I'm working on notation for an embedded logic and I'm wondering how sketchy the following is with respect to any special handling that Coq might do when parsing "forall".
Notation "'forall' x .. y , P" :=
(forall x, .. (forall y, P%type) ..) (at level 200, x binder, right associativity, only parsing) : type_scope.
Notation "'forall' x .. y , P" :=
(bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.
(forall x, .. (forall y, P%type) ..) (at level 200, x binder, right associativity, only parsing) : type_scope.
Notation "'forall' x .. y , P" :=
(bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.
Without the first rule, I seem to completely loose access to Coq's primitive forall.
I tried the following alternative where I don't put forall in single quotes:
Notation "forall x .. y , P" :=
(bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.
(bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.
But this doesn't seem to work, it either silently ignores the rule, or it ignores the %I annotation on P and attempts to parse the body using type scope.
Thanks!
gregory malecha
- [Coq-Club] Overloading the forall notation, Gregory Malecha, 04/22/2020
- Re: [Coq-Club] Overloading the forall notation, Jason Gross, 04/22/2020
Archive powered by MHonArc 2.6.18.