idris-lang/Idris-dev — pull request #767 by ahmadsalim (2014-01-05 18:44:35+00:00)
Title: Allows induction on more complicated data types 

Works with all types that have eliminators now.
Still beta-ish as not thorough testing has been done, eliminators still need to be fixed for some data types namely those with implicit arguments.

Example proof:

```Idris
vlength : Vect n a -> Nat
vlength [] = 0
vlength (_ :: xs) = S (vlength xs)

vect_is_length_indexed : {v : Vect n a} -> n = vlength v
vect_is_length_indexed = ?p_vect_is_length_indexed

---------- Proofs ----------

p_vect_is_length_indexed = proof
intros
induction v
trivial
intros
compute
rewrite ihxs
trivial
```