leanprover/lean — pull request #368 by avigad (2014-12-05 22:12:28+00:00)
Title: feat(library/data/int): replace int definition with structure and better computational behavior

I still have to do a lot of "cleanup", but at least the new definition of integers is in place.

My agenda now is:
(1) return to algebra and prove facts about ordered rings
(2) make int an instance of an ordered ring, and transfer all the properties (and refactor)
(3) refactor nat

BTW, one test is broken (coe.input), but that doesn't have anything to do with me, does it?