coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: 김형선 <hskiowa AT kaist.ac.kr>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Questions about tactics
- Date: Fri, 29 Jun 2012 17:11:54 -0400
김형선 wrote:
>
> 1. How can I search and print tactics?
I don't know of any built-in commands for searching tactics. The command
[Print Ltac] exists, though.
> 2. What are the most rudimentary (that is, defined without Ltac) of
> the tactics?
>
Many tactics are defined in OCaml for performance reasons, even if they
could be implemented from more primitive tactics in Ltac. So, your
question is either ill-defined or has too long of an answer to be useful!
If there is some specific practical motivation for your question, we
might be able to help better if you share it.
> 3. How can I make Coq print dependencies bewteen tactics,
>
> just like we do the same in definitions (theorems) using "Print
> Assumptions (qualid)/ Print Opaque Dependencies (qualid)"?
>
I don't know of any such command.
- [Coq-Club] Questions about tactics, 김형선, 06/29/2012
- Re: [Coq-Club] Questions about tactics, Adam Chlipala, 06/29/2012
Archive powered by MHonArc 2.6.18.