edwinb/Idris-dev — pull request #212 by david-christiansen (2013-03-04 12:55:10+00:00)
Title: 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.