lean-verbose

Stream: new members

[Lucas Bazante]

Hi, everyone! I'm trying to translate the Lean verbose project (https://github.com/PatrickMassot/lean-verbose) to brazilian portuguese, but I'm new to Lean and I need to understand the project a little better for the translation to work properly, and to expand the tatics if I need to.

I didn't find any documentation other than the examples provided in the Github repo, so I was wondering if anyone knew of a documentation for the project, or a publication/paper about it that might help me understand it better!

[Eric Wieser]

Note that this project is for Lean 3, which is a bad choice for new projects (or translations of old ones)

[Patrick Massot]

Yes, writing a translation of the Lean 3 version is a very bad idea. It would have been a great idea two years ago.

[Patrick Massot]

If you are really serious about wanting to use this then you should tell me and I'll rise the priority of porting this to Lean 4 so that you'll be able to translate the Lean 4 version.