Data.Comp.Param.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

Functor FreshM

Applicative FreshM

data Name

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

Instances

Eq Name

Ord Name

Show Name

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

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

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

Run the given computation with the next available name.

evalFreshM :: FreshM a -> a

Evaluate a computation that uses fresh names.