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 withing to use or to contribute to the project.

Table of contents

• What is Lambdapi?

• Installation

• Command line options

• User interfaces

• Module system

• Syntax of terms

• Syntax of commands

• Syntax of proof tactics

• API

• Structure of directories and files

• Implementation choices

• Contributing

• Compiling and profiling

• Compatibility with Dedukti

• Bibliographic references

• Including Lambdapi code into a Latex document