Def List.repeatSucc

Modification history

2021-11-22 15:44

Mathlib/Data/List/Basic.lean

feat: add simp linter (#100) …

Deleted List.repeatSucc View on Github →

2021-06-22 14:47

Mathlib/Data/List/Basic.lean

list(basic): Add repeat & repeat succ (#16)

Added List.repeatSucc View on Github →