| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.Shell.Proof
- externals :: [External]
- data UserProofTechnique
- userProofTechnique :: TransformH LCoreTC () -> UserProofTechnique
- withProofExternals :: (MonadError CLException m, MonadState CommandLineState m) => m a -> m a
- performProofShellCommand :: (MonadCatch m, CLMonad m) => ProofShellCommand -> ExprH -> m ()
- forceProofs :: (MonadCatch m, CLMonad m) => m ()
- data ProofShellCommand = PCUser UserProofTechnique
Documentation
data UserProofTechnique Source
Instances
withProofExternals :: (MonadError CLException m, MonadState CommandLineState m) => m a -> m a Source
performProofShellCommand :: (MonadCatch m, CLMonad m) => ProofShellCommand -> ExprH -> m () Source
forceProofs :: (MonadCatch m, CLMonad m) => m () Source