Fix typo in raise deprecation message (#2226)

agda · Dec 12, 2023 · 6bfa348 · 6bfa348
1 parent 2b8fff1
commit 6bfa348
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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