| Copyright | (c) Xie Ruifeng 2020 |
|---|---|
| License | AGPL-3 |
| Maintainer | krantz.xrf@outlook.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Contract.Check
Description
Synopsis
- type MonadTypeCheck m = (MonadReader ([Type], [Term]) m, MonadFail m, MonadIO m)
- runTypeCheck :: MaybeT (ReaderT ([Type], [Term]) IO) a -> IO (Maybe a)
- assert :: MonadFail m => Bool -> m ()
- prove :: MonadTypeCheck m => Term -> m ()
- typeOf :: MonadTypeCheck m => Term -> m Type
- eval1 :: [Term] -> Term -> Term
- evalWith :: [Term] -> Term -> Term
- eval :: Term -> Term
Documentation
type MonadTypeCheck m = (MonadReader ([Type], [Term]) m, MonadFail m, MonadIO m) Source #
Type checker monad.
runTypeCheck :: MaybeT (ReaderT ([Type], [Term]) IO) a -> IO (Maybe a) Source #
Run the type checker monad, get a Maybe result.
prove :: MonadTypeCheck m => Term -> m () Source #
Prove a term in the type checker monad.