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 also a typo and use of deprecated function in intro.lean #97

Closed VhRvo closed 1 year ago

VhRvo commented 1 year ago

I am so sorry, I am not familiar with git and I think the configuration on my local git is broken after my renaming, so I cannot put this commit directly in the last patch.

If you don't like this, I think I can cancel the last patch and create a new PR.