idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

docs: typo in list difference documentation (#3018)

Browse Source
This commit is contained in:
scarf 2023-07-17 00:39:36 +09:00 committed by GitHub
parent 6729fa8c89
commit 388d217757
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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/List.idr
View File

@ -279,7 +279,7 @@ infix 7 \\
||| |||
||| In the following example, the result is `[2, 4]`. ||| In the following example, the result is `[2, 4]`.
||| ```idris example ||| ```idris example
||| [1, 2, 3, 4] // [1, 3] ||| [1, 2, 3, 4] \\ [1, 3]
||| ``` ||| ```
||| |||
public export public export