coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Questions about Tactic Notations

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Kaiyu Yang <kaiyuy AT cs.princeton.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Questions about Tactic Notations
Date: Mon, 17 Dec 2018 09:19:37 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:WKjWrBafW3+9gxqtuKg+VGb/LSx+4OfEezUN459isYplN5qZoMiybnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yb4wBD+QPP+lWrIfyqFQSohalGQmgGPnixiNUinLs36A31fkqHwHc3AwnGtIDqHvarND0NKcWUOC1y7HHwzHdYPNNwy/985DHfBE7rvGIWbJ/b8XRyU43GA7ZlFWQqJbqPyiI3ekKrWeW9OVhWOGzh2I9rAFxuDevy94qh4LUhYwV0kjJ+Th6zYs2P9G0VlB3bN++HJdNtSyWKpF6Tt4sTm12oCo3yL8LtYSmcCUEyZkr3RHSZ+Cdf4SV7B/uV+CcKipiin1/YrKwnROy/FCgyuLiUsm0105HryVGn9XQrHwN0AbT6sefRvt8+EeuxyqP2hjO5uxHIk04j7TXJ4Agz7Iqi5Yes1nPEjXrlEj4kqOabkAk9fKp6+TjbLXmvJicN4pshw7gKakvlc+yDfgiPggJRWib9vyw1Kf/8k3hXLVKkvo2n7HFv5DdPMQXv7K2AwtI0ok48Bu/FDen0NEAnXYdNl5FeRSHj5LoO17UOvz4A+2/0ByQl2JIzvHXI/XQC5PCZizAmbbwYKdV4FUa0BAyy9tS+5VSTLwNPaSgdFX2sYn1Cx49MguD4ev8ms5K+YoaXW+ABZiwKqLbqhfc68o/c7HKY5Ua7mWuY8M57uLj2Cdq0WQWerOkiN5OMCjhT6ZWZn6BaH+pue8vVGIDvw4wVuvv2Q+SAWYVYGy9DftlumMLTbm+BIKGfbiDxaSb1XbpDs0OIGdcBQLUSCq6R8C/Q/4JLRmqDIphnzgDBOqxG9dn0guh5lb3
Organization: X80 Heavy Industries

Hi Kaiyu,

Kaiyu Yang
<kaiyuy AT cs.princeton.edu>
writes:

> 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?

Maybe "Print Ltac Signatures" ? It should be easy to extend that command
if you have some specific need.

SerAPI does also provide some listing facilities.

> 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.

Unfortunately, IIANM the "equational" rules that govern tactic
definitions/substitutions are a tad more complex than what one would
think so TTBOMK this is not possible nor easy to do.

Best,
E.

[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