idris-lang/Idris-dev — pull request #1189 by david-christiansen (2014-05-04 21:26:37+00:00)
Title: Apropos improvements

```
Idris> :apropos nat -> string
Prelude.Strings.length : String -> Nat
Returns the length of the string.

Idris> :apropos fin -> string

Idris> :apropos fin -> plus

Idris> :apropos fin -> +
Prelude.Fin.+ : Fin n -> Fin m -> Fin (n + m)
Add two Fins, extending the bound

Prelude.Fin.shift : (m : Nat) -> Fin n -> Fin (m + n)
Add some natural number to a Fin, extending the bound accordingly

Prelude.Fin.weakenN : (n : Nat) -> Fin m -> Fin (m + n)
Weaken the bound on a Fin by some amount
```