Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Questions about tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Questions about tactics


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page