Commit 2023-01-24 08:00 8280a0e1

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/LazyList/Basic.lean

added theorem LazyList.append_assoc

added theorem LazyList.append_bind

added theorem LazyList.append_nil

added def LazyList.attach

added def LazyList.find

added theorem LazyList.forall_mem_cons

added def LazyList.init

added def LazyList.interleave

added def LazyList.interleaveAll

added def LazyList.listEquivLazyList

added theorem LazyList.mem_cons

added theorem LazyList.mem_nil

added def LazyList.mfirst

added def LazyList.pmap

added def LazyList.reverse

added theorem Thunk.ext