leanprover-community / lean4-metaprogramming-book

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

metam: add section on type checking, type inference, typeclass inference #69

Open JLimperg opened 2 years ago

JLimperg commented 2 years ago

Another note to self: mention these functions somewhere in the MetaM chapter. There's not much to discuss, but this functionality is obviously important, so people should be able to discover it from the book.