Using lean4export

Stream: new members

[Philip Stetson]

I am having trouble running lean4export; I believe I have it installed properly and I can't understand the code well enough to diagnose it myself.

I have a build of mathlib with this dependency installed: https://github.com/leanprover/lean4export

I have imported the mathlib libraries that I want to export by calling them in the header of the Export.lean file. Although, whenever I run "lake exe lean4export" I get the error citing lean4export/Main.lean at lines 7 and 8:

"application type mismatch
importModules imports
argument
imports
has type
List ?m.237 : Type
but is expected to have type
Array Import : TypeLean 4"

I want am not sure whether I am using the package properly or if there is a bug. Please let me know if you know how to run lean4export.

[Alex J. Best]

You could try running the branch in https://github.com/leanprover/lean4export/pull/2/, I also cant work out how to use that version of export with a newer library. @Sebastian Ullrich do you plan to merge such updates into lean4export or do you have advice how to set the paths correctly to make this work as is

[Mario Carneiro]

I bumped lean4export to 4.3.0