leanprover/lean — pull request #309 by avigad (2014-11-07 20:18:15+00:00)
Title: feat(library/algebra/order): begin theory of orders

feat(library/algebra/order): begin theory of orders

I just noticed that Leo has a better definition of well-founded relations in logic.lean. I will later make this file consistent with that.

Leo, there is one comment in order.lean that shows a place where universe parameters have to be provided explicitly to make something type check. The problem is that class inference returns a solution with the wrong variables. I don't know if there is a nice fix, but it is worth taking a look.

Aside from a bundle command, I can think of other bells and whistles that might make structures easy to use. E.g. suppose I have shown that a type is a group. Right now the only way to show it is a commutative group is to use the use the constructor for commutative group. It might be nice to have another constructor simply take a group and a proof that the multiplication is commutative. (But this is not critical and can be postponed.)