coq-zipper

An attempt to verify the Zipper

• The Derivative of a Regular Type is its Type of One-Hole Contexts (http://strictlypositive.org/diff.pdf, [ McBride2001 ])

Any results?

• A tree over a type T is pretty zippable and a zipper over a tree will preserve all the desired properties and modifications. Tree is ( T(A, R) -> 1 + A * list(R) )