idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

:browse doesn't show instances #2587

Open david-christiansen opened 9 years ago

david-christiansen commented 9 years ago

:browse at the REPL should really show which instances are defined as well.

cbiffle commented 9 years ago

While it's Christmas, :doc Foo showing the instances defined for Foo would also be lovely. :-)

david-christiansen commented 9 years ago

@cbiffle You're in luck! It's Christmas early!

Idris> :doc Functor
Type class Functor
    Functors

Parameters:
    f   -- the action of the functor on objects

Methods:
    map : Functor f => (m : a -> b) -> f a -> f b
        The action of the functor on morphisms

        The function is Total
Instances:
    Functor List
    Functor (IO' ffi)
    Functor Stream
    Functor Provider
    Functor Binder
    Functor Elab
    Functor PrimIO
    Functor Maybe
    Functor (Either e)

Subclasses:
    Traversable f
    Applicative f

This was there in the latest release already.

cbiffle commented 9 years ago

Sorry if I was imprecise. When working with a type T it is currently difficult to discover which typeclasses, if any, T is an instance of. On Sep 10, 2015 2:12 PM, "David Christiansen" notifications@github.com wrote:

@cbiffle https://github.com/cbiffle You're in luck! It's Christmas early!

Idris> :doc Functor Type class Functor Functors

Parameters: f -- the action of the functor on objects

Methods: map : Functor f => (m : a -> b) -> f a -> f b The action of the functor on morphisms

    The function is Total

Instances: Functor List Functor (IO' ffi) Functor Stream Functor Provider Functor Binder Functor Elab Functor PrimIO Functor Maybe Functor (Either e)

Subclasses: Traversable f Applicative f

This was there in the latest release already.

— Reply to this email directly or view it on GitHub https://github.com/idris-lang/Idris-dev/issues/2587#issuecomment-139380713 .

ahmadsalim commented 8 years ago

Wow, I didn't even know about :browse. Is this undocumented?

jfdm commented 8 years ago

I think browse is documented in the help, but not really elsewhere. Might be good at some point to improve the manual with information about searching and browsing of Idris code.