Arthur Paulino

We don't have a html link yet. I'll talk to the core devs about hosting the book like they do with the other Lean 4 books

More: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Metaprogramming.20tutorial/near/292051009

I think we can close this one

Oh it's been so long! Unfortunately, at this point, I have less context than @ytzfhqs ):

It would definitely be a honorable effort of great help! Please don't forget to add yourself as an author if you do so 👍🏼

better beach sounds: https://soundbible.com/tags-beach.html

If there's a file in focus that doesn't have its current `olean` up to date, I assume there will be work happening in the background. Won't the background job conflict...

Yeap, thanks!

More context: #732 did this because the sha256 coprocessor code was replicated in three different places (benchmark + ivc example + nivc example). Now that it's centralized, it's easier for...

Sure, you can go for the minimal PR and then we evaluate the need of subsequent PRs afterwards. Thanks for opening the issue!