From cd303cd8e5d491426511037a40b06324412afaad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Oct 2022 16:43:10 -0700
Subject: [PATCH] fix: do not apply `simpAppApp?` over cast

---
 src/Lean/Compiler/LCNF/Simp/SimpValue.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
index aa2fa43189..d533eea51e 100644
--- 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