idris-lang/Idris-dev — pull request #1544 by david-christiansen (2014-09-24 12:59:29+00:00)
Title: Nicer-looking disambiguation in :printdef

Now, it only shows full names in cases of ambiguity.
```
Idris> :printdef (++)
Prelude.List.(++) : List a -> List a -> List a
([] ++ right) = right
((x :: xs) ++ right) = (x :: (xs ++ right))

Prelude.Strings.(++) : String -> String -> String
(++) = prim__concat

Prelude.Vect.(++) : Vect m a -> Vect n a -> Vect (m + n) a
([] ++ ys) = ys
((x :: xs) ++ ys) = (x :: (xs ++ ys))
Idris> :printdef plus
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)
Idris> :printdef Vect
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
Idris> :printdef Nil
Prelude.List.Nil : List a

Prelude.Vect.Nil : Vect 0 a
Idris> :printdef (::)
Prelude.List.(::) : a -> List a -> List a

Prelude.Stream.(::) : a ->
Lazy' LazyCodata (Stream a) -> Stream a

Prelude.Vect.(::) : a -> Vect n a -> Vect (S n) a
Idris> :printdef LTE
data LTE : Nat -> Nat -> Type where
lteZero : LTE 0 right
lteSucc : LTE left right -> LTE (S left) (S right)
```