minor PR for lean4-metaprogramming-book

Stream: new members

[Krishna Padmasola]

Hi, I am trying to learn Lean programming and am really happy with the quality of the books. I came across a minor typo in the tactics chapter for which I raised a PR. Please let me know if it is acceptable. I would like to learn by contributing, so if you can suggest any beginner friendly issues, I'd really appreciate it. Thank you!

[Julian Berman]

Welcome! I think that looks good, appreciated. Waiting for CI to pass and then will merge.

[Julian Berman]

I think it's useful if you share your goals/background a bit! I assume when you say you're trying to learn Lean programming -- is that specifically in contrast to using Lean for mathematics? But yeah your background may help others have ideas for how you can help!

[Krishna Padmasola]

Thanks @Julian Berman. I am employed in the software industry. My work involves programming in Java. I have also used C/C++/Python in the past. Few years ago I came across Haskell and since then I have been trying to wrap my head around it. Lean seems very similar. I am curious about the theorem proving aspect of it and the meta programming part.

I do have some background in Math and Physics, having studied Physics at graduate level, but that was a while back :-). My math skills at this point may not suffice for using Lean for Math proofs, but I should be able to contribute to any programming related tasks/issues.

[Adomas Baliuka]

There's a few open PRs on that repo (disclosure: two by me) so I had thought it's not really maintained anymore. Very glad to hear it is! It's a nice book about a topic that's (for me) really hard to learn by comparison. :heart:

[Julian Berman]

So I'm happy to merge PRs but am careful with them given I... haven't had a chance to read the book! But if they're trivial you're welcome to ping me (here or on the pr)

[Adomas Baliuka]

@Julian Berman my PRs would be lean4-metaprogramming-book/#144 and lean4-metaprogramming-book/#143

• 143 is just slightly improved wording and removes a repeated word "a".
• 144 is about an error (wrong universe levels) in a code example (discussed here)

[Krishna Padmasola]

@Julian Berman I opened another minor PR here: https://github.com/leanprover-community/lean4-metaprogramming-book/pull/146. Can you please review when you get a chance? Thanks!

[Julian Berman]

I left a small comment. Thanks for the PR!

[Krishna Padmasola]

@Julian Berman Thanks for your review comments. I applied the suggested change and updated the PR.