| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.Dictionary.WorkerWrapper.Common
- externals :: [External]
- data WWAssumptionTag
- data WWAssumption = WWAssumption WWAssumptionTag (RewriteH CoreExpr)
- assumptionAClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Clause
- assumptionBClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Clause
- assumptionCClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Clause
- split1BetaR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr
- split2BetaR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr
- workLabel :: LemmaName
Documentation
data WWAssumptionTag Source
data WWAssumption Source
Constructors
| WWAssumption WWAssumptionTag (RewriteH CoreExpr) |
assumptionAClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Clause Source
assumptionBClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Clause Source
assumptionCClauseT :: (BoundVars c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Clause Source
split1BetaR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source
split2BetaR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source