idris-lang/Idris-dev — pull request #1541 by david-christiansen (2014-09-24 07:32:22+00:00)
Title: Pretty-printer improvements

The pretty-printer now correctly annotates the output of :t when it's applied to a name, which means that IDE clients can now support normalization and selective showing of implicits.

Additionally, pretty-printing (=) now correctly shows implicits when that option is enabled:
```
λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
(a : Type) ->
(n : Nat) ->
(m : Nat) ->
(o : Nat) ->
(xs : Vect n a) ->
(ys : Vect m a) -> (zs : Vect o a) -> xs ++ ys ++ zs = (xs ++ ys) ++ zs : Type
λΠ> :set showimplicits
λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
(a : Type) ->
(n : Prelude.Nat.Nat) ->
(m : Prelude.Nat.Nat) ->
(o : Prelude.Nat.Nat) ->
(xs : Prelude.Vect.Vect n a) ->
(ys : Prelude.Vect.Vect m a) ->
(zs : Prelude.Vect.Vect o a) ->
(=) {A = Prelude.Vect.Vect (Prelude.Nat.plus n (Prelude.Nat.plus m o)) a}
{B = Prelude.Vect.Vect (Prelude.Nat.plus (Prelude.Nat.plus n m) o) a}
(Prelude.Vect.(++) {m = n}
{a = a}
{n = Prelude.Nat.plus m o}
xs
(Prelude.Vect.(++) {m = m} {a = a} {n = o} ys zs))
(Prelude.Vect.(++) {m = Prelude.Nat.plus n m}
{a = a}
{n = o}
(Prelude.Vect.(++) {m = n} {a = a} {n = m} xs ys)
zs) : Type
```
This fixes #1410.