search

leanprover-community / lean4-metaprogramming-book

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

There is a typo and use of deprecated function in `intro.md` #96

Closed VhRvo closed 1 year ago

VhRvo commented 1 year ago
  1. There is no symbol constructor;
  2. Lean.Meta.intro1P has been deprecated, use Lean.MVarId.intro1P .
arthurpaulino commented 1 year ago

Can you do those changes on the corresponding lean file as well? Or build the markdown files

VhRvo commented 1 year ago

Can you do those changes on the corresponding lean file as well? Or build the markdown files

I am so sorry I have to create a new PR to change the corresponding lean file.

arthurpaulino commented 1 year ago

@VhRvo no, you just need to push a new commit to this branch of yours with the new changes