IdrisDoc: Data.List.Zipper

# Data.List.Zipper

A Zipper implementation for Lists
inspired by
https://hackage.haskell.org/package/ListZipper-1.2.0.2/docs/src/Data-List-Zipper.html

data Zipper : Type -> Type

  A Zipper for Lists

  Zip : List a -> List a -> Zipper a
cursor : Zipper a -> Maybe a

  gets the element at the current cursor

      cursor $ fromList [1,2,3,4,5]

delete : Zipper a -> Zipper a

  delete the element at the current cursor

      show $ Data.List.Zipper.delete $ fromList [1,2,3,4,5]

empty : Zipper a

  creates an empty Zipper

      empty {a = Nat}

end : Zipper a -> Zipper a

  move the cursor to the end of the Zipper

      show $ end $ fromList [1,2,3,4,5]

endp : Zipper a -> Bool

  checks whether the cursor is at the end of the Zipper

      endp $ fromList [1,2,3,4,5]

fromList : List a -> Zipper a

  creates a Zipper from a List

      show $ fromList [1,2,3,4,5]

index : Zipper a -> Nat

  Return the index of the current cursor

      index $ fromList [1,2,3,4,5]

insert : a -> Zipper a -> Zipper a

  inserts an element at the current cursor

      show $ insert 0 $ fromList [1,2,3,4,5]

isEmpty : Zipper a -> Bool

  checks whether this Zipper is empty

      isEmpty empty {a = Nat}

left : Zipper a -> Zipper a

  moves the cursor to the left or leaves the cursor unchanged

      show $ left $ fromList [1,2,3,4,5]

pop : Zipper a -> Zipper a

  pop an element from the Zipper

      show $ pop $ right $ fromList [1,2,3,4,5]

push : a -> Zipper a -> Zipper a

  push an element into the Zipper and move the cursor past it

      show $ push 0 $ fromList [1,2,3,4,5]

replace : a -> Zipper a -> Zipper a

  remove an element from the zipper

      show $ replace 9 $ fromList[1,2,3,4,5]

right : Zipper a -> Zipper a

  moves the cursor to the right or leaves the cursor unchanged

      show $ right $ fromList [1,2,3,4,5]

start : Zipper a -> Zipper a

  move the cursor to the start of the Zipper

      show $ start $ fromList [1,2,3,4,5]

startp : Zipper a -> Bool

  checks whether the cursor is at the start of the Zipper

      startp $ fromList [1,2,3,4,5]

toList : Zipper a -> List a

  convert this Zipper to a list

      toList $ fromList[1,2,3,4,5]