Def List.rdrop

Modification history

2023-11-17 05:53

Mathlib/Data/List/DropRight.lean

chore: bump to v4.3.0-rc2 (#8366) …

Added List.rdrop View on Github →

2023-11-07 10:14

Mathlib/Data/List/Rdrop.lean

chore: rename List.rdrop to dropRight (#8233) …

Deleted List.rdrop View on Github →

2023-01-10 15:05

Mathlib/Data/List/Rdrop.lean

feat: port Data.List.Rdrop (#1382)

Added List.rdrop View on Github →