idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 05:01:34 +03:00
Code Issues Projects Releases Wiki Activity

Fix typo in documentation string

Browse Source
This commit is contained in:
hilary888 2022-09-30 21:11:02 +00:00 committed by G. Allais
parent b697cea6e2
commit 9eaff9f728
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/Vect.idr
View File

@ -207,7 +207,7 @@ unsnoc : (xs : Vect (S n) a) -> (Vect n a, a)
unsnoc [x] = ([], x) unsnoc [x] = ([], x)
unsnoc (x :: xs@(_ :: _)) = let (ini, lst) = unsnoc xs in (x :: ini, lst) unsnoc (x :: xs@(_ :: _)) = let (ini, lst) = unsnoc xs in (x :: ini, lst)
||| Repeate some value some number of times. ||| Repeat some value some number of times.
||| |||
||| @ len the number of times to repeat it ||| @ len the number of times to repeat it
||| @ x the value to repeat ||| @ x the value to repeat