Pattern-Matching Expressions directly🔗

In Metaprogramming, for instance for writing tactics, it is often necessary to see whether an expression matches a certain pattern. Lean provides several Recognizers that can be used to check if an expression matches a certain pattern and to extract the relevant sub-expressions. For example, the function Expr.isAppOf checks if an expression is an application of a certain function and extracts the arguments of the application.

1. Example : Splitting goals in ∧