Commit 2022-06-20 22:02 125055b0

View on Github →

refactor(data/sym/basic): change notation for sym.cons (#14853) Switch from :: to ::ₛ for sym.cons so that it no longer conflicts with list.cons. This (finally) puts it in line with other notations, like ::ₘ for multiset.cons.

Estimated changes

Modified src/data/sym/basic.lean

modified theorem sym.coe_cons

modified theorem sym.cons_inj_left

modified theorem sym.cons_inj_right

modified theorem sym.cons_of_coe_eq

modified theorem sym.cons_swap

modified theorem sym.exists_eq_cons_of_succ

modified theorem sym.mem_cons

modified theorem sym.mem_cons_of_mem

modified theorem sym.mem_cons_self

modified theorem sym.repeat_succ