Data.Comp.MultiParam.FreshM

This module defines a monad for generating fresh, abstract names, useful e.g. for defining equality on terms.

Documentation

data FreshM a

Monad for generating fresh (abstract) names.

Instances

Monad FreshM

data Name i

Abstract notion of a name (the constructor is hidden).

Instances

PEq Name

POrd Name

Eq (Name i)

Ord (Name i)

Show (Name i)

(EqHD f, PEq a) => PEq (Cxt h f Name a)

(OrdHD f, POrd a) => POrd (Cxt h f Name a)

withName :: (Name i -> FreshM a) -> FreshM a

Run the given computation with the next available name.

nameCoerce :: Name i -> Name j

Change the type tag of a name.

evalFreshM :: FreshM a -> a

Evaluate a computation that uses fresh names.