什么是元编程？
贡献者：subfish-zhou
Lean 中的元编程指编写能够操作其他代码的程序。由于代码用字符串表示，最朴素的元编程方式就是直接操作字符串。但这样做非常容易出错，也不够强大和高效。
因此，元编程操作的是代码的内部表示。在 Lean 中，代码的内部表示有两个层次：语法（Syntax）与表达式（Expressions）（在多数其他语言中操作的是抽象语法树）。较简单的元编程形式是操作语法（即所谓的宏），更强大的形式是操作表达式。本手册中的配方会覆盖这两个层次的元编程，但大多数配方都在表达式这一层。
配方：