idris-lang/Idris-dev — pull request #1543 by david-christiansen (2014-09-24 12:21:40+00:00)
Title: Major improvements to pretty-printing and :printdef

The pretty-printer no longer ugly-prints `let ... in ...` expressions. Additionally, :printdef now supports data, codata, and constructor definitions, and the IDE protocol supports retrieving definitions, with a test implementation of "show definition" in the right-click menu for names in `idris-mode`.

Examples:
```
λΠ> :printdef (::)
(::) : a -> List a -> List a
(::) : a -> Lazy' LazyCodata (Stream a) -> Stream a
(::) : a -> Vect n a -> Vect (S n) a
λΠ> :printdef Vect
data Prelude.Vect.Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
λΠ> :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))
λΠ> :printdef plusAssociativeStepCase
Prelude.Nat.plusAssociativeStepCase : (left : Nat) ->
(centre : Nat) ->
(right : Nat) ->
(left + (centre + right) = left + centre + right) ->
S (plus left (plus centre right)) =
S (plus (plus left centre) right)
plusAssociativeStepCase = \left =>
\centre =>
\right =>
\inductiveHypothesis =>
let {rewrite_rule109} = inductiveHypothesis
in replace rewrite_rule refl
λΠ> :printdef plusAssociative
Prelude.Nat.plusAssociative : (left : Nat) ->
(centre : Nat) ->
(right : Nat) -> left + (centre + right) = left + centre + right
plusAssociative 0 centre right = refl
plusAssociative (S left) centre right = let inductiveHypothesis =
plusAssociative left centre right
in plusAssociativeStepCase left
centre
right
inductiveHypothesis
```