search

leanprover-community / lean4-metaprogramming-book

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

typos(lean/main/tactics.lean): some typos #80

Closed adomani closed 1 year ago

adomani commented 1 year ago

I am more confident with these than with the other PR: they are probably all typos!

arthurpaulino commented 1 year ago

Nice! Can you run the Python script to update the markdown files as well please?

adomani commented 1 year ago

If I understood correctly how to use lean2md, this should be done!

arthurpaulino commented 1 year ago

Thanks!