直接对表达式进行模式匹配🔗

贡献者：Siddhartha Gadgil, subfish-zhou

在元编程中，例如编写策略时，常常需要判断一个表达式是否匹配某个模式。Lean 提供了若干识别器（Recognizers），可用来检查一个表达式是否匹配某个模式并提取相关的子表达式。例如，函数 Expr.isAppOf 检查一个表达式是否是某个函数的应用，并提取该应用的参数。