Writing a tactic with Camltac#

In this tutorial, you’ll learn how to write a simple Camltac tactic that behaves like Lean’s apply? tactic, suggesting lemmas to apply in the current goal. We’ll cover:

  • How to setup a Dune project for Camltac;

  • How to execute Camltac code;

  • How to use pattern-matching, Ltac2 APIs, and Rocq APIs in Camltac;

  • How to import your tactic in other files;

  • How to export your tactic to Ltac2.

Start the tutorial with the setup.