fix: do not apply simpAppApp? over cast

2022-10-09 16:43:10 -07:00 · 2022-10-09 16:43:10 -07:00 · cd303cd8e5
commit cd303cd8e5
parent cf313d2101
1 changed files with 1 additions and 0 deletions
--- a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
@ -32,6 +32,7 @@ def simpAppApp? (e : Expr) : OptionT SimpM Expr := do
  guard f.isFVar
  let f ← findExpr f
  guard <| f.isApp || f.isConst
+  guard <| !f.isAppOf ``lcCast
  markSimplified
  return mkAppN f e.getAppArgs