comparator

Stream: lean4

[Jason Gross]

Has anyone gotten the comparator to work when Quot.sound is involved? I am trying to figure out whether uncaught exception: (kernel) unknown constant 'Eq' is a bug in the compartor, lean4export, or lean4checker

[Henrik Böving]

I've previously used comparator to check results from Mathlib so it is certainly possible yes, lean4export also manages to correctly export Quot.sound from the module based from a cursory look at its output so I would suspect that this is an issue with the replay system from lean4checker. Though also a very specific issue because only in the very minimal configurations that you use does Eq not get added through some other mean before Quot.sound pops up eventually.

[Henrik Böving]

CC @Kim Morrison if something in the lean4checker codebase regarding dependencies of axioms comes to mind.