Zulip Chat Archive

Stream: PrimeNumberTheorem+

Topic: lean_exe build target?

David Renshaw (Jan 30 2024 at 16:45):

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/9

David Renshaw (Jan 30 2024 at 16:46):

I'm guessing that the only reason for the lean_exe is that lake init put it there?

Ian Jauslin (Jan 31 2024 at 00:15):

Yes indeed. Thank you!

Last updated: May 02 2025 at 03:31 UTC