Lambdapi User Manual

Lambdapi is a proof assistant for the λΠ-calculus modulo rewriting. See What is Lambdapi? for more details.

Lambdapi files must end with .lp. But Lambdapi can also read Dedukti files ending with .dk and convert them to Lambdapi files (see Compatibility with Dedukti).

Installation instructions - Frequently Asked Questions - Issue tracker

Learn Lambdapi in 15 minutes

Examples of developments made with Lambdapi:

• Some logic definitions

• Library on natural numbers, integers and polymorphic lists

• Example of inductive-recursive type definition

• Example of inductive-inductive type definition

• Test files

Opam repository of Lambdapi libraries

• What is Lambdapi?
• Getting started
• Command line interface

• User interfaces
  • Emacs
  • VSCode
  • Vim (not maintained anymore)

• Module system
• Syntax of terms
• Commands
• Proof mode
• Proof tactics
• Proof tactics on equality
• Tacticals
• Queries
• Query Language
• Compatibility with Dedukti
• Include Lambdapi code in a Latex document

For developers

Guidelines for contributing

• Overview of directories and files
• Implementation choices
• Decision trees
• Testing
• Profiling

Indices and tables

• Index

• Search Page