reference type checker

Stream: lean4

[Jakob von Raumer]

Is anyone unbeknownst to me already working on a reference type checker for Lean 4 or an a suitable export format for a reference type checker? trepplein4, @Gabriel Ebner ?

[Mario Carneiro]

I believe nanoda supports lean 4, but it hasn't been touched in a while, and I'm not sure what the status of the extensions to the export format are

[Jakob von Raumer]

But that still seems to refer to the old export format, right?

[Gabriel Ebner]

I think the old export format is the new export format: https://github.com/leanprover-community/mathlib4/blob/d1ab52522f2161afdf5b4d28af8499747e7e990b/Mathlib/Util/Export.lean (with some small changes ofc.)

[Jakob von Raumer]

Ah thanks!