Skip to content

Commit 94abfa5

Browse files
alexariceandreasabel
authored andcommitted
Fix typo in raise deprecation message (#2226)
1 parent 24370a3 commit 94abfa5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/Fin/Base.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -317,7 +317,7 @@ compare (suc i) (suc j) with compare i j
317317
raise = _↑ʳ_
318318
{-# WARNING_ON_USAGE raise
319319
"Warning: raise was deprecated in v2.0.
320-
Please use _↑ instead."
320+
Please use _↑ʳ_ instead."
321321
#-}
322322
inject+ : {m} n Fin m Fin (m ℕ.+ n)
323323
inject+ n i = i ↑ˡ n

0 commit comments

Comments
 (0)