Def LazyList.init

Modification history

2024-07-15 23:26

Mathlib/Data/LazyList/Basic.lean

chore: bump dependencies (upstream LazyList) (#14778) …

Deleted LazyList.init View on Github →

2023-01-24 08:00

Mathlib/Data/LazyList/Basic.lean

feat: port Data.LazyList.Basic (#1776)

Added LazyList.init View on Github →