From 94abfa5fb3ec04df9a0c0c19c4ad39738d74433e Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Tue, 12 Dec 2023 16:47:45 +0000
Subject: [PATCH] Fix typo in raise deprecation message (#2226)

---
 src/Data/Fin/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 9b4c303f2f..d762e10007 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -317,7 +317,7 @@ compare (suc i) (suc j) with compare i j
 raise = _↑ʳ_
 {-# WARNING_ON_USAGE raise
 "Warning: raise was deprecated in v2.0.
-Please use _↑_ʳ instead."
+Please use _↑ʳ_ instead."
 #-}
 inject+ : ∀ {m} n → Fin m → Fin (m ℕ.+ n)
 inject+ n i = i ↑ˡ n