Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-20 21:42 a30b7c77

View on Github →

feat(data/string): fix string_lt, add repr for multiset, pnat

Estimated changes

Created data/char.lean

Modified data/finset.lean

Modified data/list/basic.lean

added theorem list.lex.append_left

added theorem list.lex.append_right

added theorem list.lex.cons_iff

modified theorem list.lex.imp

added theorem list.lex.ne_iff

added theorem list.lex.to_ne

modified inductive list.lex

deleted theorem list.lex_append_left

deleted theorem list.lex_append_right

deleted theorem list.lex_ne_iff

deleted theorem list.ne_of_lex_ne

added theorem list.nil_lt_cons

modified theorem list.reverse_cons'

modified theorem list.reverse_cons

Modified data/list/perm.lean

Modified data/multiset.lean

Modified data/pnat.lean

Created data/string.lean

added theorem string.le_iff_to_list_le

added theorem string.lt_iff_to_list_lt

added def string.ltb

added theorem string.to_list_inj

Modified order/basic.lean

modified theorem is_order_connected.neg_trans

modified theorem is_strict_weak_order_of_is_order_connected