Search results

The modifier associative commutative can be slow with large terms

Status: Open.

#1200 In Deducteam/lambdapi;

· NotBad4U opened on Feb 13, 2025

Improve why3 tactic

feature request

Status: Open.

#1187 In Deducteam/lambdapi;

· fblanqui opened on Jan 28, 2025

Rewriting rules do not compute correctly on term defined by a set tactic ?

Status: Open.

#1178 In Deducteam/lambdapi;

· NotBad4U opened on Jan 21, 2025

print unif_rule; freezes/bug the feedback of vscode about type checking decorations/info of symbols

Status: Open.

#1167 In Deducteam/lambdapi;

· 1337777 opened on Dec 24, 2024

Installing via Cygwin fails

Status: Open.

#1162 In Deducteam/lambdapi;

· AkihisaYamada opened on Dec 17, 2024

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

Status: Open.

#1160 In Deducteam/lambdapi;

· 1337777 opened on Dec 11, 2024

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

Status: Open.

#1159 In Deducteam/lambdapi;

· 1337777 opened on Dec 11, 2024

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

emacs

feature request

vscodeIssues related to Vscode pluginIssues related to Vscode plugin

Status: Open.

#1156 In Deducteam/lambdapi;

· fblanqui opened on Nov 22, 2024

add shortcuts/menus in emacs/vscode for some commands

emacs

feature request

vscodeIssues related to Vscode pluginIssues related to Vscode plugin

Status: Open.

#1155 In Deducteam/lambdapi;

· fblanqui opened on Nov 22, 2024

do not print coercions

feature request

Status: Open.

#1154 In Deducteam/lambdapi;

· fblanqui opened on Nov 19, 2024

rewrite tactic raises "Assertion failed" in infer.ml

Status: Open.

#1152 In Deducteam/lambdapi;

· fblanqui opened on Nov 19, 2024

rewrite tactic fails when the equation contains several metavariables

Status: Open.

#1151 In Deducteam/lambdapi;

· fblanqui opened on Nov 19, 2024