Search results

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

LICENSE missing

Status: Open.

#28 In leanprover/comparator;

· Coda-Coda opened on Apr 10, 2026

comparator doesn't work when repo contains filenames starting with numbers

Status: Open.

#17 In leanprover/comparator;

· mo271 opened on Feb 13, 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