Agda.Utils.Pointer

Documentation

data Ptr a

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 a

derefPtr :: Ptr a -> a

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

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

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