coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Locate printing-only notations

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Locate printing-only notations
Date: Mon, 16 Sep 2019 11:57:49 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f42.google.com
Ironport-phdr: 9a23:SVzBPRGUxfgo6UxDX7gji51GYnF86YWxBRYc798ds5kLTJ7zpMWwAkXT6L1XgUPTWs2DsrQY0rGQ6vurADdZqdbZ6TZeKcYKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZsJ6or1xfErHREd/lYyG91OFmfmwrw6tqq8JNs7ihcpegt+9JcXan/Yq81UaFWADM6Pm4v+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAOUBM+hWrIfzukUAogelCAa2GO/i0CVFimPq0aA41ekqDAHI3BYnH9ILqHnZsM76NKcTUeCuzKnH0zbDZO5K1Df78ofIdA0uquyLUL1qasXRyUgvFxjFjlqOqozpJSma1uIXvGid8uVsT+Ovi287qwF+uTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV1b9mkEJ5KuCGbMYt7Wt8tQ2ZyuCY81LIGvZq7cDIUx5s62h7SbeGMfYuQ4h/7SuqdPTN1iGhmdb+/nRq+7Emtx+zmWsS7zlpHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzwXT5ftFIUAwjKbbKpkhzqMpmpodvknPADX6mErxjK+ReUUk/van5/77bbXho5+QL450igfgPaQygsGzH/g0PwwUU2WY+emwzqDv8Ez4TblQgfA6jLHVsJXAKsQaoq65DRVV0oEm6xunFTipy9QYnXgcLFJFZh2HjJLlNEvIIP/iC/ewnk6gkDZqx/DaMb3sGZrNLn3Zn7fgebZx8VJTyA02zdxH/ZJbFqkBIO7vWk/2rNHXEhg5MxWtz+n7DNV9y5gRVHmUAq6ZNaPSqUWH6vguI+mKfo8VuSzyJ+Ir5/703jcFngoWerDs1p8KYjjsFfN/Zk6dfHDEg9EbEG5MsBBoH8Lwj1jXeDRTZm2yUqF0zzcyDo7uWY7JRoG2gLGCmi69F5taIGFHFl+kHnLhdoHCUPAJPnHBavR9myAJAODyA7Qq0guj4Vejl+hXa9HM8yhdjqrNkcBv7rSKxx43/D1wSc+a1jPVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUBR9NW7vJNFAw9MMyFlrEoO5XJQgvEO+yxZhOmT9GhW2xjS9swx5oPZB84FYn4yB/E2CWuDvkekLnZXJE=

Locate says "unknown notation" for printing-only notations. Is there a workaround?

Notation "&&&&" := 2 (only printing).
Locate "&&&&". (* unknown notation *)

Notation "&&&" := 2.
Locate "&&&". (*Notation "&&&" := S (S O) (default interpretation) *)

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] Locate printing-only notations, Abhishek Anand, 09/16/2019