lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
metam: add section on type checking, type inference, typeclass inference
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.