Search results

Hypotheses lists and syntax broken after replacing set.mm

Status: Open.

#188 In metamath/metamath-knife;

· ProgramCrafter opened on Feb 3, 2026

Parse trees are in source order instead of argument order

Status: Open.

#170 In metamath/metamath-knife;

· digama0 opened on Oct 28, 2024

Top-level disjoint variable restrictions apply backwards

Status: Open.

#163 In metamath/metamath-knife;

· bmmoore opened on Jul 3, 2024

write_stmt_use in axiom_use.rs hates uncompressed proofs.

Status: Open.

#160 In metamath/metamath-knife;

· arpie-steele opened on Jun 15, 2024

ql.mm grammar is broken

Status: Open.

#141 In metamath/metamath-knife;

· digama0 opened on Sep 30, 2023

Wrong axioms considered in usage

Status: Open.

#124 In metamath/metamath-knife;

· tirix opened on Sep 7, 2023

Statement parse errors in some set.mm versions

Status: Open.

#121 In metamath/metamath-knife;

· tirix opened on Jul 4, 2023

Improve disjoint variable error message

Status: Open.

#109 In metamath/metamath-knife;

· tirix opened on May 20, 2023

Proof editing features

Status: Open.

#100 In metamath/metamath-knife;

· digama0 opened on Feb 19, 2023

MM Diff

Status: Open.

#99 In metamath/metamath-knife;

· tirix opened on Feb 19, 2023

Work Variables

Status: Open.

#87 In metamath/metamath-knife;

· tirix opened on Apr 27, 2022

parallel parsing mishandles repeated includes

Status: Open.

#81 In metamath/metamath-knife;

· tirix opened on Apr 4, 2022