Search results

Proof irrelevance is not respected in statements

Status: Open.

#59 In leanprover/comparator;

· eric-wieser opened on Jul 17, 2026

Comparator generates different instance names for problem and solution files

Status: Open.

#58 In leanprover/comparator;

· eric-wieser opened on Jul 17, 2026

Incorrectly adding propext with nanoda kernel

Status: Open.

#51 In leanprover/comparator;

· stephen-huan opened on Jun 6, 2026

Better errors when the lean4export version is incorrect

enhancementNew feature or requestNew feature or request

Status: Open.

#33 In leanprover/comparator;

· robsimmons opened on Apr 20, 2026

Display both types in "Challenge and solution theorem statement do not match"

Status: Open.

#9 In leanprover/comparator;

· JasonGross opened on Dec 22, 2025

comparator should permit dependent challenges ("Const does not match" is sometimes a lie)

Status: Open.

#4 In leanprover/comparator;

· JasonGross opened on Dec 20, 2025

"uncaught exception: Challenge and solution constant kind don't match" is both unhelpful and untrue

Status: Open.

#3 In leanprover/comparator;

· JasonGross opened on Dec 19, 2025