3 commits

Author	SHA1	Message	Date
Leonardo de Moura	70bd95d931	feat(library/data/list): show that (sort R l1 = sort R l2) when R is a decidable total order and l1 is a permutation of l2	2015-08-09 23:36:08 -07:00
Leonardo de Moura	2a22c75e52	feat(library/data/list/sort): prove that (sort R l) is strongly_sorted	2015-08-09 23:36:07 -07:00
Leonardo de Moura	276771e6ca	feat(library/data/list/sort): add sort for lists ... TODO: prove the result is sorted, prove that l1 ~ l2 -> sort R l1 = sort R l2	2015-08-09 14:23:09 -07:00