edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 12:54:28 +03:00
Code Issues Projects Releases Wiki Activity

Use idiom brackets in Traversable (Vect k).

Browse Source
This commit is contained in:
Matus Tejiscak 2020-04-29 08:53:30 +02:00
parent cab5497ce2
commit e0e1cb9a21
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

@ -801,7 +801,7 @@ implementation {k : Nat} -> Monad (Vect k) where
export
implementation Traversable (Vect n) where
traverse f [] = pure []
traverse f (x :: xs) = pure (::) <*> (f x) <*> (traverse f xs)
traverse f (x :: xs) = [| f x :: traverse f xs |]
--------------------------------------------------------------------------------
-- Elem