Search results

Improve why3 tactic

feature request

Status: Open.

#1187 In Deducteam/lambdapi;

· fblanqui opened on Jan 28, 2025

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

Extend associative/commutative modifiers and infix notation to symbols taking additional implicit arguments

feature request

Status: Open.

#1137 In Deducteam/lambdapi;

· fblanqui opened on Oct 4, 2024

Adding ordered rewrite system and conditional rewriting?

discussion

feature request

Status: Open.

#1133 In Deducteam/lambdapi;

· NotBad4U opened on Sep 16, 2024

Add export to the new ARI format

feature request

Status: Open.

#1102 In Deducteam/lambdapi;

· fblanqui opened on Apr 28, 2024

Coq export for symbol with definition defined with tactics

feature request

Status: Open.

#1057 In Deducteam/lambdapi;

· NotBad4U opened on Feb 27, 2024

Exporting refined signatures

feature request

Status: Open.

#1031 In Deducteam/lambdapi;

· gabrielhdt opened on Jan 24, 2024

Printing of metavariable names

error message

feature request

Status: Open.

#1021 In Deducteam/lambdapi;

· thiagofelicissimo opened on Nov 22, 2023

Having Inductive type living in Prop?

feature request

Status: Open.

#1014 In Deducteam/lambdapi;

· NotBad4U opened on Oct 13, 2023

Allow rewrite tactic on hypotheses

feature request

tacticproblems about tacticproblems about tactic

Status: Open.

#671 In Deducteam/lambdapi;

· QGarchery opened on May 12, 2021