Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-16 14:05 11bcaeb6

View on Github →

refactor(data/lazy_list): lazy_list was moved back to core lib

Estimated changes

deleted def lazy_list.append
deleted def lazy_list.approx
deleted def lazy_list.filter
deleted def lazy_list.for
deleted def lazy_list.head
deleted def lazy_list.join
deleted def lazy_list.map
deleted def lazy_list.map₂
deleted def lazy_list.nth
deleted def lazy_list.of_list
deleted def lazy_list.singleton
deleted def lazy_list.tail
deleted def lazy_list.to_list
deleted def lazy_list.zip
deleted inductive lazy_list