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

Fix typo in namespace for [bi]traversable composition

Browse Source
This commit is contained in:
Joel Berkeley 2023-09-19 18:40:05 +01:00 committed by CodingCellist
parent dc79c6dd05
commit f6c000e27e
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libs/prelude/Prelude/Interfaces.idr
View File

@ -583,8 +583,7 @@ namespace Traversable
using Foldable.Compose Functor.Compose where
traverse = traverse . traverse
namespace Bitraveresable
namespace Bitraversable
||| Composition of a bitraversable and a traversable is bitraversable.
public export %tcinline
[Compose] (l : Traversable t) => (r : Bitraversable p) => Bitraversable (t .: p)