Lean4迭代器实现代码求评审及优化建议

我正在学习Lean4——这门兼具函数式编程和定理证明器特性的语言。因为Lean4没有内置迭代器（或无限列表）这类实用数据结构，我自己动手实现了一套迭代器，还完成了斐波那契序列的迭代器版本，但素数筛的实现目前无法正常运行。

考虑到Lean4的线上相关资源比较匮乏，能写出这套代码对我来说已经是不小的成果，现在恳请各位帮忙评审我的代码，并给出优化建议。

内容的提问来源于stack exchange，提问作者khanh