Search results

LSP: Proof decomposition should push ' down

enhancementA new feature, an improvement, or other addition.A new feature, an improvement, or other addition.

Status: Open.

#261 In tlaplus/tlapm;

· kape1395 opened on Apr 15, 2026

New warning ld: warning: ignoring duplicate libraries: '-lc++', '-lpthread'

Status: Open.

#259 In tlaplus/tlapm;

· ahelwer opened on Apr 13, 2026

TLAPM library modules depend on community modules

Status: Open.

#252 In tlaplus/tlapm;

· ahelwer opened on Mar 1, 2026

TLAPM fails when instantiating a module containing ENABLEDaxioms (Error: Operator "EnabledWrapper" not found)

Status: Open.

#250 In tlaplus/tlapm;

· qdelamea-aneo opened on Feb 3, 2026

Can't solve even when conclusion matches assumption exactly

Status: Open.

#247 In tlaplus/tlapm;

· talex5 opened on Dec 19, 2025

When run from a different directory, TLAPM cannot handle leading text on modules imported using EXTENDS

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#245 In tlaplus/tlapm;

· ahelwer opened on Dec 16, 2025

Tuple quantification should not be supported in ASSUME NEW <<x, y>> \in S statements

bugAn error, usually in the code.An error, usually in the code.

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#242 In tlaplus/tlapm;

· ahelwer opened on Oct 31, 2025

TLAPM parser incorrectly allows LAMBDA as expression

bugAn error, usually in the code.An error, usually in the code.

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#238 In tlaplus/tlapm;

· ahelwer opened on Sep 4, 2025

TLAPM parser incorrectly accepts recursive operator when it is a function literal

bugAn error, usually in the code.An error, usually in the code.

semantic checkerIssues relating to TLAPM's resolution of semantic propertiesIssues relating to TLAPM's resolution of semantic properties

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#237 In tlaplus/tlapm;

· ahelwer opened on Sep 4, 2025

TLAPM parser silently drops expressions of form e \in S when parsing finite set literals

bugAn error, usually in the code.An error, usually in the code.

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#235 In tlaplus/tlapm;

· ahelwer opened on Jul 28, 2025

Replace TLAPM parser with SANY

semantic checkerIssues relating to TLAPM's resolution of semantic propertiesIssues relating to TLAPM's resolution of semantic properties

syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parser

Status: Open.

#213 In tlaplus/tlapm;

· ahelwer opened on May 27, 2025

Error while proving Some(x, op)' = Some(x', op') when op is an operator.

Status: Open.

#207 In tlaplus/tlapm;

· kape1395 opened on Mar 15, 2025