coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Questions about Tactic Notations

From: Kaiyu Yang <kaiyuy AT cs.princeton.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Questions about Tactic Notations
Date: Sat, 15 Dec 2018 23:58:51 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kaiyuy AT cs.princeton.edu; spf=Pass smtp.mailfrom=kaiyuy AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:iL10OBam5xUFyZUmOp5G3gT/LSx+4OfEezUN459isYplN5qZoM+ybnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE28G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYY4VAOoAPedYspT2qFkUohu4CgmnGeTiyjxSiX/33aw6zuQgHBra0ww7Bd4OqG7UrNTzNKgOT++10K7IzTPZY/xIxDj99ZHFfxY8qv+PRbJ9adfdxVcsGg/fk1mctJLpMymI2ukDsmWX9ehtWfy3h2I5tw18piKjy8Qsh4XTmI4Z1E7I+T95zYs7I9CzVVR1bsS+EJRKsiGXL4t2Td0mQ2FvoCs6xacGtoClcygMzJQnxhHfa/ybc4SS/h3jT/ydIS9ihHJkfrKwmwi98VSnyu36TMW7zktFrjddntnNsHACyQDT59CaRvdj/UqtwyuD2x3N5u1ePEw5m6vWJ4Qjz7IujpYTtF7MHi7ymEX4lq+WcUAk9/Cr6+v9Y7XnpoKcNo9vhw7iKaQigNS/Af45MggIQ2eU5/i81Lrl/UHjXrpFk+A2nrHDsJ/GPcQburK5AwhN34k/7Ba/Fi6q38gcnXkaN11IYwmHjojsO1HWOv/0F/a/g1K2kDdq3f/KJLPhAo+eZkTExbzmZPN271NW4As119FWoZxOWZ8bJ/emeUbwpcGQPxY/PETgwO/mGchs/ogFH3qVA6mSPb/VtxmF6v95cLrEX5McpDuoc6tt3PXpl3JswQZML5ns5oMebTWDJtojJkyYZXT2hdJYQTUBpUwmVu3sg1CeVjgVanqvDftlumMLTbm+BIKGfbiDxaSb1X7rTJZNIHhcC1aHHGvvccOJV+peMHvPcP8kqSQNUP2ac6Fk1Ryqs1WrmbV9I+fS/iwXtY6l38Mz//fSkxo/6TtyScmRzjPVQg==

Hello guys,

I have a few questions about tactic notations:

1. Is it possible to print all the tactic notations in the environment? (pretty much like what "Print Ltac Signatures" do for Ltac). I know one can potentially use "Print Grammar tactic", but is there a more straightforward way?

2. Is it possible to run alpha-reduction and beta-reduction to eliminate the tactic notations? Or is there something similar to "Unset Printing Notations" that works for tactic notations.

Thank you very much!

Best,

Kaiyu Yang
Ph.D. student in computer science at Princeton University
35 Olden Street, Room 431

Princeton, NJ 08540
+1 (734)389-9696

[Coq-Club] Questions about Tactic Notations, Kaiyu Yang, 12/16/2018
- Re: [Coq-Club] Questions about Tactic Notations, Emilio Jesús Gallego Arias, 12/17/2018