| 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 = PCEnd ProofReason
- data ProofReason = UserProof 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
data ProofReason Source
Constructors
| UserProof UserProofTechnique | Run the technique, mark Proven if succeeds |