search

leanprover-community / lean4-metaprogramming-book

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

`md` parameter of `whnf'` is unused #55

Closed dwrensha closed 2 years ago

dwrensha commented 2 years ago

In the MetaM chapter, whnf' has an unused md parameter:

https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/b7762483d16577eb2f25d6a57942f76054acb578/lean/main/metam.lean#L621-L625

It looks to me like this should be removed.

Lower down, the transparency mode is controlled via withTransparency:

https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/b7762483d16577eb2f25d6a57942f76054acb578/lean/main/metam.lean#L647

cc @JLimperg, who added this section as part of #34.

arthurpaulino commented 2 years ago

Yes we can remove it. @dwrensha do you want to make the PR?

JLimperg commented 2 years ago

Indeed this was left over from an earlier version of the text. Thank you for the fix!