ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Pointer

1 type
5 values

PackageAgda-2.7.0.1
Exports6
LanguageHaskell2010
LicenceMIT
SourcePointer.hs

datadata Ptr a

Instances8Functor, Foldable, Traversable, Eq, Ord, Show, …

Functor PtrDefined in Agda-2.7.0.1 · Agda.Utils.Pointer
Foldable PtrDefined in Agda-2.7.0.1 · Agda.Utils.Pointer
Traversable PtrDefined in Agda-2.7.0.1 · Agda.Utils.Pointer
Eq (Ptr a)Defined in Agda-2.7.0.1 · Agda.Utils.Pointer
Ord (Ptr a)Defined in Agda-2.7.0.1 · Agda.Utils.Pointer
Show a => Show (Ptr a)Defined in Agda-2.7.0.1 · Agda.Utils.Pointer
NFData (Ptr a)Defined in Agda-2.7.0.1 · Agda.Utils.Pointer
Hashable (Ptr a)Defined in Agda-2.7.0.1 · Agda.Utils.Pointer

valuenewPtr :: a -> Ptr a

valuederefPtr :: Ptr a -> a

valuesetPtr :: a -> Ptr a -> Ptr a

valueupdatePtr :: (a -> a) -> Ptr a -> Ptr a

valueupdatePtrM :: Functor f => (a -> f a) -> Ptr a -> f (Ptr a)

If f a contains many copies of a they will all be the same pointer in the result. If the function is well-behaved (i.e. preserves the implicit equivalence, this shouldn't matter).