OTOH, the complete documentation for the "map" function in #Idris is: "The action of the functor on morphisms".
-
-
Replying to @andreasdotorg
@andreasdotorg Ugh. As if that's more useful than just looking at the type… I'd better look over the whole Prelude for this sort of thing.2 replies 0 retweets 3 likes -
Replying to @edwinbrady
@edwinbrady@andreasdotorg This was my fault a while back when I was playing with diagrams in docstrings - the text managed to survive. Sry.2 replies 0 retweets 2 likes -
Replying to @d_christiansen
@d_christiansen@andreasdotorg I deliberately didn't look up who to blame :). Hopefully the new version is informative anyway.3 replies 0 retweets 1 like -
Replying to @edwinbrady
@edwinbrady BTW, I proved false today: https://github.com/idris-lang/Idris-dev/issues/2716 …1 reply 0 retweets 2 likes
@d_christiansen Oh yes, %reflection functions are never total (or, as you say, even really functions). All sorts of things will break.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.