idris-lang/Idris-dev — pull request #713 by ahmadsalim (2013-12-10 12:05:08+00:00)
Title: Added support for induction tactic (works only for nonparameterized types insofar, requires eliminator for type)

We can now do proofs like these:
```Idris
ELIMTest.pluscommutes_proof = proof
intros
induction n
compute
rewrite (n_plus_O m)
trivial
intros
compute
rewrite (sym iht__0)
rewrite (n_plus_S_m m t__0)
trivial
```