Safe Haskell | None |
---|---|

Language | Haskell2010 |

- emitPreCond :: Require -> Ivory eff ()
- emitPostCond :: Ensure -> Ivory eff ()
- newtype Cond = Cond {}
- check :: IBool -> Cond
- checkStored' :: forall ref s a c. (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => (c -> Cond) -> ref s (Stored a) -> (a -> c) -> Cond
- class CheckStored c where
- class Requires c where
- requires' :: (WrapIvory m, Requires c, IvoryType r) => (c -> Cond) -> c -> m r -> m r
- class Ensures c where
- ensures' :: (WrapIvory m, Ensures c, IvoryVar r) => (c -> Cond) -> (r -> c) -> m r -> m r
- ensures_' :: (WrapIvory m, Ensures c) => (c -> Cond) -> c -> m () -> m ()

# Documentation

emitPreCond :: Require -> Ivory eff () Source #

Emit a pre-condition.

XXX do not export

emitPostCond :: Ensure -> Ivory eff () Source #

Emit a post-condition.

XXX do not export

checkStored' :: forall ref s a c. (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => (c -> Cond) -> ref s (Stored a) -> (a -> c) -> Cond Source #

class CheckStored c where Source #

class Requires c where Source #

Proc bodies that have pre-conditions. Multiple pre-conditions may be provided, for which the conjunction must hold.