a4d41beab1
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. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||