My Ltac2 Tutorials

Posted on June 19, 2024
Tags: ,

I always wanted to have my Ltac2 tutorials on Github indexed by the search engine, but unfortunately, instead of indexing my tutorials, Google indexed an unfinished Ltac2 blog post that I forgot to remove from my Hakyll cache :(

Instead, please refer to my repository for an alternative to some existing tutorials such as https://github.com/tchajed/ltac2-tutorial and the Ltac2 official documentation.

My tutorial focuses on the very basics of programming with Ltac2 as an ML-family langauge so you can easily transfer knowledge about ML-like languages (e.g. Gallina, OCaml, Haskell) to Ltac2. The goal of the tutorials is to help you see that Ltac2 is nothing more than a nice ML language with a nice set of APIs for interacting with the Coq proof state.

You can access the HTML version of the tutorial here: https://electriclam.com/ltac2/toc.html