From 66be8b9d4cd8aaa6e332a2c6398ddcf6ef38beeb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 23 Feb 2024 21:14:17 -0800
Subject: [PATCH] fix: `ToExpr` instance for `Fin`

---
 src/Lean/ToExpr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 36406fe57b..7d226b8108 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -48,7 +48,7 @@ instance : ToExpr (Fin n) where
   toExpr a :=
     let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
-      (mkApp2 (.const ``Fin.instOfNat []) (mkRawNatLit (n-1)) r)
+      (mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
 
 instance : ToExpr (BitVec n) where
   toTypeExpr := .app (mkConst ``BitVec) (toExpr n)