Individuazione della definizione di una tattica nelle prove Coq

Question

Nello studio delle prove di Coq di altri autori, incontro spesso una tattica, diciamo "inv eq Heq" o "intro_b". Voglio capire queste tattiche.

Come posso trovare se è una tattica Coq o una notazione tattica definita da qualche parte nel mio progetto corrente?

In secondo luogo, c'è un modo per trovare la sua definizione?

Ho utilizzato SearchAbout, Search, Locate e Print ma non sono riuscito a trovare le risposte alle domande precedenti.

Answer 1

Si dovrebbe essere in grado di utilizzare

Print Ltac <tacticname>. 

per stampare il codice di una tattica definita dall'utente (in base al documentation).

---

per trovare dove si è definito ... Credo che si sta andando ad avere bisogno di grep purtroppo, Locate non funziona per tattiche nomi sembra.

Answer 2

Come accennato in precedenza, Print Ltac ... stampa il codice di una tattica definita dall'utente.

Per individuare una tattica definita dall'utente (ovvero per sapere dove è definita), utilizzare Locate Ltac .... Ti dà il nome completo. Quindi utilizzare Locate Library per trovare il file corrispondente.