Merge branch 'master' into bump/nightly-2024-10-17

leanprover-community · Oct 18, 2024 · e141ac3 · e141ac3
2 parents 0495948 + 1357f4f
commit e141ac3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
@@ -17,11 +17,11 @@ private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
 
 instance [ReduceEval α] : ReduceEval (List α) := ⟨evalList⟩
 
-instance : ReduceEval (Fin (n+1)) where
+instance [NeZero n] : ReduceEval (Fin n) where
   reduceEval := fun e => do
     let e ← whnf e
     if e.isAppOfArity ``Fin.mk 3 then
-      return Fin.ofNat (← reduceEval (e.getArg! 1))
+      return Fin.ofNat' _ (← reduceEval (e.getArg! 1))
     else
       throwFailedToEval e