Issues

• add checking of doc compilation in CI

  Deducteam/lambdapi#1533 · Filter by author fblanqui opened on Oct 9, 2026
  

• typo in directory name

  Deducteam/lambdapi#1531 · Filter by author fblanqui opened on Oct 9, 2026
  

• Problems with Emacs

  emacs
  Deducteam/lambdapi#1528 · Filter by author fblanqui opened on Oct 6, 2026
  1

  

• capture of global variables

  Deducteam/lambdapi#1515 · Filter by author bodeveix opened on Sep 17, 2026

• naming conflicts

  Deducteam/lambdapi#1514 · Filter by author bodeveix opened on Sep 16, 2026

• allow open an alias ?

  Deducteam/lambdapi#1511 · Filter by author fblanqui opened on Sep 12, 2026

• Equality type remains unresolved during conversion despite typed arguments

  Deducteam/lambdapi#1503 · Filter by author melanie-taprogge opened on Sep 4, 2026

• Rewrite tactic fails to match equality when both sides are lambda terms

  Deducteam/lambdapi#1487 · Filter by author melanie-taprogge opened on Aug 7, 2026
  2

• lambdapi upstream does not compile when installed with opam

  Deducteam/lambdapi#1482 · Filter by author sacerdot opened on Jul 31, 2026
  4

  

• Problem with escaped module names

  Deducteam/lambdapi#1481 · Filter by author fblanqui opened on Jul 28, 2026

• Virtual positions for generated symbols

  Deducteam/lambdapi#1451 · Filter by author fblanqui opened on Jul 10, 2026

• Dk/Lp modules: use zlexbuf instead of lexbuf

  Deducteam/lambdapi#1449 · Filter by author fblanqui opened on Jul 9, 2026

• Lpo files contain absolute positions

  Deducteam/lambdapi#1436 · Filter by author Alidra opened on Jul 2, 2026
  4

• feature request: allow require commands in mapping files for lambdapi export --mapping

  feature request
  Deducteam/lambdapi#1351 · Filter by author fblanqui opened on Feb 15, 2026

• make odoc does not generate links to every module

  Deducteam/lambdapi#1335 · Filter by author fblanqui opened on Dec 13, 2025
  

• Inefficient handling of let's in reduction and conversion

  Deducteam/lambdapi#1324 · Filter by author NotBad4U opened on Nov 25, 2025
  8

• VS Code extension fails to display goals due to unfinished lines in proof-scripts

  lsp
  Deducteam/lambdapi#1218 · Filter by author melanie-taprogge opened on Mar 13, 2025
  1

  

• The modifier associative commutative can be slow with large terms

  Deducteam/lambdapi#1200 · Filter by author NotBad4U opened on Feb 13, 2025
  1

• Improve why3 tactic

  feature request
  Deducteam/lambdapi#1187 · Filter by author fblanqui opened on Jan 28, 2025

• Installing via Cygwin fails

  Deducteam/lambdapi#1162 · Filter by author AkihisaYamada opened on Dec 17, 2024
  3

• higher-order rewrite rule with implicit arguments under the binder: uninformative cryptic error message? BUG?

  Deducteam/lambdapi#1160 · Filter by author 1337777 opened on Dec 11, 2024
  2

• unif_rule is unable to bypass the priority of injectivity unification vs rewriting reduction? BUG?

  Deducteam/lambdapi#1159 · Filter by author 1337777 opened on Dec 11, 2024
  2

• emacs/vscode: automatically add/remove {}'s after a tactic when there are too few/many subproofs

  emacsfeature requestvscode
  Deducteam/lambdapi#1156 · Filter by author fblanqui opened on Nov 22, 2024
  

• add shortcuts/menus in emacs/vscode for some commands

  emacsfeature requestvscode
  Deducteam/lambdapi#1155 · Filter by author fblanqui opened on Nov 22, 2024
  

• do not print coercions

  feature request
  Deducteam/lambdapi#1154 · Filter by author fblanqui opened on Nov 19, 2024