Standard library of Lambdapi

November 17, 2025 ยท View on GitHub

  • Prop: propositional logic
  • Eq: equality
  • Set: set codes for polymorphism
  • FOL: typed first-order logic
  • Bool: booleans
  • Nat: natural numbers
  • List: polymorphic lists
  • Classic: classical logic

The libraries on natural numbers and polymorphic lists follow the corresponding Coq SSReflect libraries:

Installation with Opam

opam repository -a --set-default add lambdapi https://github.com/deducteam/opam-lambdapi-repos
itory.git # once
opam install lambdapi-stdlib

Usage in Lambdapi

require open Stdlib.Prop Stdlib.Set Stdlib.FOL Stdlib.Nat /* ... */;

Compilation from the sources

opam install --deps-only . # once
make

Installation from the sources

opam install .