02b206af9b
This PR ensures that `mkAppM` can be used to construct terms that are only type-correct at at default transparency, even if we are in `withReducible` (e.g. in simp), so that simp does not stumble over simplifying `let` expression with simplifiable type.reliable. Here is a reproducer of the issue this solves: ``` example (a b : Nat) (h : a = b): (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by simp -zeta -zetaDelta [h] ``` This fixes #7826. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||