Commit 2021-09-17 20:09 54217b6a

View on Github →

chore(data/list): make separate lexicographic file (#9193) A minor effort to reduce the data.list.basic monolithic, today inspired by yet again being annoyed that I couldn't find something.

Estimated changes

Modified src/data/list/basic.lean

deleted theorem decidable.list.lex.ne_iff

deleted theorem list.lex.append_left

deleted theorem list.lex.append_right

deleted theorem list.lex.cons_iff

deleted theorem list.lex.imp

deleted theorem list.lex.ne_iff

deleted theorem list.lex.not_nil_right

deleted theorem list.lex.to_ne

deleted inductive list.lex

deleted theorem list.nil_lt_cons

Created src/data/list/lex.lean

added theorem decidable.list.lex.ne_iff

added theorem list.lex.append_left

added theorem list.lex.append_right

added theorem list.lex.cons_iff

added theorem list.lex.imp

added theorem list.lex.ne_iff

added theorem list.lex.not_nil_right

added theorem list.lex.to_ne

added inductive list.lex

added theorem list.nil_lt_cons

Modified src/data/list/pairwise.lean

Modified src/data/string/basic.lean

Modified src/order/lexicographic.lean