Export the implementation of `Traversable (Vect k)`

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris

https://idris-lang.org/

Other

902 stars 58 forks source link

Export the implementation of `Traversable (Vect k)` #337

Closed ziman closed 4 years ago

ziman commented 4 years ago

For some reason, it was hidden but it's useful. (I need it.)

edwinb commented 4 years ago

Oops! I think when this happens it results from the %access directives in Idris 1, but I decided we shouldn't have them in Idris 2 because it's too easy to export things by accident that way.