search

leanprover-community / lean4-metaprogramming-book

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

Minor typo #115

Closed pkshashank closed 5 months ago

pkshashank commented 11 months ago

The target of ?m3 should be f a = a.

Seasawher commented 5 months ago

@Julian @pkshashank This should be closed as completed:

see ad53e6fd2fd742e436cb56232120a8f902df8385

Julian commented 5 months ago

Indeed.