search

leanprover-community / lean4-metaprogramming-book

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

metam: fix wrong explanation of WHNF #51

Closed JLimperg closed 2 years ago

JLimperg commented 2 years ago

Also some formatting fixes.

As discussed here: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.E2.9C.94.20WHNF.20of.20partially.20applied.20constants

JLimperg commented 2 years ago

Rish's fix made this PR mostly redundant, so now it's largely stylistic improvements.

JLimperg commented 2 years ago

Thanks! I'll keep this in mind for future PRs.