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.
2 files changed