From b7efd200f0f0ece09ed612c8465065b8231e80ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 2 Jan 2024 05:17:20 -0800
Subject: [PATCH] chore: typo

---
 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
index 759163d82c..32c60a5323 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
@@ -20,7 +20,7 @@ def fromExpr? (e : Expr) : SimpM (Option Value) := do
   unless type.isAppOfArity ``Fin 1 do return none
   let some size ← evalNat type.appArg! |>.run | return none
   unless size > 0 do return none
-  let some value ← evalNat e.appFn!.appArg! |>.run | return none
+  let some value ← Nat.fromExpr? e.appFn!.appArg! | return none
   let value := value % size
   return some { size, value, ofNatFn := e.appFn!.appFn! }