leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
213 stars 53 forks source link

add "run on Lean4 Playground" button #136

Closed Seasawher closed 2 weeks ago

Seasawher commented 6 months ago

Add the button 'Run in Lean4 Playground' to all code blocks and each page. Clicking it will take you to the Lean 4 web.

I don't know how useful this is; However, being able to jump to Lean 4 web significantly lowers the barrier to editing the code examples yourself.