Mohit Tekriwal (May 30 2022 at 23:44): Mohit Tekriwal (May 30 2022 at 23:44):Hi, I just started exploring the Ltac language in Coq. Could someone help me with pointing to a tutorial/resources to learn the tactic language for beginners? Thank you !!
Michael Soegtrop (May 31 2022 at 07:20):For Ltac1 would recommend (http://adam.chlipala.net/cpdt/html/Cpdt.Match.html).
For Ltac2 there is not much as yet, but at the tactic level it is reasonably close to Ltac and at the programming level it is reasonably close to OCaml, so if you know both, it is not hard to get along with Ltac2. For clarification of not so obvious things I usually consult the test files in the Coq repo (https://github.com/coq/coq/tree/master/test-suite/ltac2) and if this doesn't help, I ask here.
Mohit Tekriwal (May 31 2022 at 13:02):Thank you @Michael Soegtrop !!
Last updated: Oct 12 2024 at 13:01 UTC