Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 04:59 755cb75f

View on Github →

feat(data/list/basic): non-meta to_chunks (#7517) A non-meta definition of the list.to_chunks method, plus some basic theorems about it.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.to_chunks_aux_eq

added theorem list.to_chunks_aux_join

added theorem list.to_chunks_eq_cons'

added theorem list.to_chunks_eq_cons

added theorem list.to_chunks_join

added theorem list.to_chunks_length_le

added theorem list.to_chunks_nil

Modified src/data/list/defs.lean

added def list.to_chunks

added def list.to_chunks_aux