renamed homomorphism to morphism
Add inductive integers

This is inspired by Agda's integers. An integer is defined as a positive Nat
or the negative successor of a Nat, yielding unique 0 and fairly convenient
definitions of operations.
Merge pull request #212 from david-christiansen/inductive-ints

Add inductive integers
Generate legal DChkCase expressions when defunctionalization is trivial
Fix some big number primitives
Fixes issue #177
Some RTS functions to help with allocation in foreign functions
Merge pull request #211 from raichoo/morph

renamed homomorphism to morphism
Merge pull request #214 from bitlisp/trivialdefun

Generate legal DChkCase expressions when defunctionalization is trivial
Change argument order for mkStrFn
Update version number to 0.9.7
Minor tutorial updates
evTree does not handle ImpossibleCase
Check the type of a proof matches the type of the goal!
Merge pull request #218 from raichoo/master

trivial fix
vim: added reflect tactic
vim: added tactics block
Merge pull request #219 from raichoo/master

Some vim adjustments
Backend support for Java
Missing case in Idris.Parser

This module:




    module main




    using (A : Type) 
      data W : Type where
        Ok : (r : A -> A -> Type) -> W




gave the error 




    src/Idris/Parser.hs:(215,23)-(223,86): Non-exhaustive patterns in case
    
which seemed to be repaired by this amendment for the [] case.
Merge pull request #221 from JanBessai/master

Backend support for Java