DOCUMENTATION.md

User manual for Lambdapi

Lambdapi is a proof assistant based on the λΠ-calculus modulo rewriting, mostly compatible with the proof checker Dedukti. This document provides a good starting point for anyone wishing to use or to contribute to the project.

Table of contents

• What is Lambdapi?

• Installation

• Getting started

• Command line options

• User interfaces

  • Emacs

  • VSCode

  • Vim

  • Atom

• Module system

• Syntax of terms

• Commands

• Tactics

• Compatibility with Dedukti

• Bibliographic references

• Including Lambdapi code into a Latex document

For developers:

• Contributing

• Overview of directories and files

• Implementation choices

• Compiling and profiling