Zulip Chat Archive

Stream: Is there code for X?

Topic: Zippers

cognivore (Jul 27 2022 at 21:14):

There are a lot of interesting things in lean4 tests, for example, there's a concrete ListZipper α \text{ListZipper } \alpha . In Haskell they have generic Zippers. I wonder if someone implemented those in Lean 4?

Eric Wieser (Jul 27 2022 at 21:51):

Can you link to the one in the lean4 test?

Last updated: Dec 20 2023 at 11:08 UTC