Zulip Chat Archive

Stream: new members

Topic: lean-verbose

Lucas Bazante (Oct 02 2023 at 21:44):

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 (Oct 02 2023 at 21:57):

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

Patrick Massot (Oct 02 2023 at 22:04):

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 (Oct 02 2023 at 22:05):

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.

Last updated: Dec 20 2023 at 11:08 UTC