perf: `match_expr` join points We use `let_delayed` to elaborate `match_expr` join points, which elaborate the body of the `let` before its value. Thus, there is a difference between: - `let_delayed f (x : Expr) := <val>; <body>` - `let_delayed f := fun (x : Expr) => <val>; <body>` In the latter, when `<body>` is elaborated, the elaborator does not know that `f` takes an argument of type `Expr`, and that `f` is a function. Before this commit ensures the former representation is used.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.