Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-07 10:10 2f2e016e

View on Github →

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

  • chore(data/list/basic): rename take_all -> take_length
  • also rename drop_all

Estimated changes

deleted theorem list.drop_all
added theorem list.drop_length
deleted theorem list.take_all
added theorem list.take_length