Post #1865896

@jnkrtech The Haskell stuff is pretty abstract, yeah. The Idris bits are fairly concrete, the only real abstraction is the "element type". It's almost the "standard" catenable deque (in the form of a 2-3 finger tree). "Almost" because it's for type-aligned relations instead of "mere" homogeneous values. I also have the "standard" catenable deque in Idris directly translated from the literature ("Purely Function Data Structures" by Okasaki): https://stefan-hoeck.github.io/idris2-pack-db/docs/okasaki-pfds/docs/docs/SimpleCatenableDeque.src.html An illustration of semi-mutual recursion (not mine) is on Stack Overflow: https://stackoverflow.com/a/36911924 Best of luck; if you have questions I'll try to answer.