fix: panic at reducePow

closes #4947
leanprover · Aug 12, 2024 · aa4dfbb · aa4dfbb
1 parent 4236d8a
commit aa4dfbb
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -55,8 +55,9 @@ builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDi
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
-  let some n ← fromExpr? e.appFn!.appArg! | return .continue
-  let some m ← fromExpr? e.appArg! | return .continue
+  let_expr HPow.hPow _ _ _ _ n m := e | return .continue
+  let some n ← fromExpr? n | return .continue
+  let some m ← fromExpr? m | return .continue
   unless (← checkExponent m) do return .continue
   return .done <| toExpr (n ^ m)
 

diff --git a/tests/lean/run/4947.lean b/tests/lean/run/4947.lean
@@ -0,0 +1,6 @@
+universe u
+class G (A : outParam Nat) where Z : Type u
+export G (Z)
+abbrev f (a : Nat) : Nat := 2 ^ a
+variable [G (f 0)]
+example {s : Z} : s = s := by simp only [Nat.reducePow]