Safe Haskell	None
Language	Haskell98

Agda.Utils.Pointer

Synopsis

Documentation

data Ptr a Source

Instances

Functor Ptr Source
Foldable Ptr Source
Traversable Ptr Source
Eq (Ptr a) Source
Ord (Ptr a) Source
Show a => Show (Ptr a) Source
NFData (Ptr a) Source
Hashable (Ptr a) Source
TermLike a => TermLike (Ptr a) Source
Subst a => Subst (Ptr a) Source
Apply a => Apply (Ptr a) Source
AbstractTerm a => AbstractTerm (Ptr a) Source

newPtr :: a -> Ptr a Source

derefPtr :: Ptr a -> a Source

setPtr :: a -> Ptr a -> Ptr a Source

updatePtr :: (a -> a) -> Ptr a -> Ptr a Source

updatePtrM :: Functor f => (a -> f a) -> Ptr a -> f (Ptr a) Source

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).