Safe Haskell	None

Agda.Utils.Pointer

Synopsis

Documentation

data Ptr a Source

Instances

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

newPtr :: a -> Ptr aSource

derefPtr :: Ptr a -> aSource

setPtr :: a -> Ptr a -> Ptr aSource

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

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