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 !!
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.
Thank you @Michael Soegtrop !!
Last updated: Jan 31 2023 at 10:01 UTC