Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.take_length

Modification history

2020-04-07 10:10

src/data/list/basic.lean

chore(data/list/basic): rename take_all -> take_length (#2343) …

Added list.take_length View on Github →