Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- data WWAssumptionTag
- data WWAssumption = WWAssumption WWAssumptionTag (RewriteH CoreExpr)
- assumptionAEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Equality
- assumptionBEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Equality
- assumptionCEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Equality
- split1BetaR :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr
- split2BetaR :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr
- workLabel :: RememberedName
Documentation
data WWAssumptionTag Source
assumptionAEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Equality Source
assumptionBEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Equality Source
assumptionCEqualityT :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Equality Source
split1BetaR :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source
split2BetaR :: (BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source