Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- data WWAssumptionTag
- data WWAssumption = WWAssumption WWAssumptionTag (RewriteH CoreExpr)
- assumptionAQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Quantified
- assumptionBQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Quantified
- assumptionCQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Quantified
- split1BetaR :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr
- split2BetaR :: (BoundVars c, HasHermitMEnv m, HasHscEnv 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
assumptionAQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> Transform c m x Quantified Source
assumptionBQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Quantified Source
assumptionCQuantifiedT :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m) => CoreExpr -> CoreExpr -> CoreExpr -> Transform c m x Quantified Source
split1BetaR :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source
split2BetaR :: (BoundVars c, HasHermitMEnv m, HasHscEnv m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> CoreExpr -> CoreExpr -> Rewrite c m CoreExpr Source