Ltac2

What is Ltac2?

Ltac2 is a meta-programming language designed to write reliable and predictable proof script. It is the replacement for Ltac1 which had unclear semantics, lacked expressivity, and was slow and error-prone.

In particular, it features:

• A ML language with a strict type system, and datatypes like list or array
• A predictable call by value semantic
• Effects to manipulate the proof state, backtracking and terms
• A nice foreign-function interface to expose .ml code in Ltac2
• It comes with a core library that exposes many .ml function of the kernel to manipulate goals, terms, etc., like unification

Tutorials

Introductions

• A Brief Introduction to ML like languages
• A brief introduction to manipulating tactics and thunking in Ltac2 interactive version and source code
• Introduction to Ltac2

Features

• Quoting in Ltac2
• Matching Terms and Goals in Ltac2 interactive version and source code
• Backtracking in Ltac2 interactive version and source code
• Notations in Ltac2

How-to Guides

• How to write a contradiction tactic with Ltac2 interactive version and source code