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

• Module system

• Syntax of terms

• Commands

• Tactics

• Editing Lambdapi source code with Emacs

• Structure of directories and files

• Implementation choices

• Contributing

• Compiling and profiling

• Compatibility with Dedukti

• Bibliographic references

• Including Lambdapi code into a Latex document