Stream: Ltac2

Topic: Resources to learn Ltac/Ltac2


view this post on Zulip 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 !!

view this post on Zulip 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.

view this post on Zulip Mohit Tekriwal (May 31 2022 at 13:02):

Thank you @Michael Soegtrop !!


Last updated: Jan 31 2023 at 10:01 UTC