Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.xfc4e5982026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · fc4e598 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Zipper

2 types
1 class

PackageAgda-2.8.0.2
Exports3
LanguageHaskell2010
LicenceMIT

classclass Zipper z where

Associated types

type family Carrier z
type family Element z

Methods

firstHole :: Carrier z -> Maybe (Element z, z)
plugHole :: Element z -> z -> Carrier z
nextHole :: Element z -> z -> Either (Carrier z) (Element z, z)

Instances3Zipper

Zipper (ElimZipper a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce.Fast
Zipper (ListZipper a)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
(Zipper f, Zipper g, Element f ~ Carrier g) => Zipper (ComposeZipper f g)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper

datadata ListZipper a

Constructors

ListZip [a] [a]

Instances9Functor, Foldable, Traversable, Eq, Ord, Show, …

Functor ListZipperDefined in Agda-2.8.0.2 · Agda.Utils.Zipper
Foldable ListZipperDefined in Agda-2.8.0.2 · Agda.Utils.Zipper
Traversable ListZipperDefined in Agda-2.8.0.2 · Agda.Utils.Zipper
Eq a => Eq (ListZipper a)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
Ord a => Ord (ListZipper a)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
Show a => Show (ListZipper a)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
Zipper (ListZipper a)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
type Carrier (ListZipper a) = [a]Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
type Element (ListZipper a) = aDefined in Agda-2.8.0.2 · Agda.Utils.Zipper

datadata ComposeZipper f g

Constructors

ComposeZip f g

Instances3Zipper, Carrier, Element

(Zipper f, Zipper g, Element f ~ Carrier g) => Zipper (ComposeZipper f g)Defined in Agda-2.8.0.2 · Agda.Utils.Zipper
type Carrier (ComposeZipper f g) = Carrier fDefined in Agda-2.8.0.2 · Agda.Utils.Zipper
type Element (ComposeZipper f g) = Element gDefined in Agda-2.8.0.2 · Agda.Utils.Zipper