Commit 2021-12-31 19:13 e4607f8f

View on Github →

chore(data/sym/basic): golf and add missing simp lemmas (#11160) By changing cons to not use pattern matching, (a :: s).1 = a ::ₘ s.1 is true by rfl, which is convenient here and there for golfing.

Estimated changes

Modified src/data/setoid/basic.lean

Modified src/data/sym/basic.lean

modified def sym.cons

added theorem sym.cons_erase

added theorem sym.eq_repeat

added theorem sym.exists_mem

deleted def sym.mem

modified def sym.nil

deleted def sym.of_vector

added theorem sym.of_vector_cons

added theorem sym.of_vector_nil