Safe Haskell | None |
---|---|
Language | Haskell98 |
Documentation
class (Applicative m, Monad m) => Freshable m a where Source #
Instances
Freshable m Integer => Freshable m RReft Source # | |
(Freshable m Integer, Monad m, Applicative m) => Freshable m Reft Source # | |
(Freshable m Integer, Monad m, Applicative m) => Freshable m Expr Source # | |
(Freshable m Integer, Monad m, Applicative m) => Freshable m Symbol Source # | |
Freshable CG Integer Source # | This is all hardwiring stuff to CG ---------------------------------------- |
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # | |
(Freshable m Integer, Monad m, Applicative m) => Freshable m [Expr] Source # | |
refreshArgs :: FreshM m => SpecType -> m SpecType Source #
refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)]) Source #
refreshArgsSub :: FreshM m => SpecType -> m (SpecType, Subst) Source #