Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Utils.Pointer

Synopsis

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

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