Safe Haskell | None |
---|---|
Language | Haskell2010 |
- 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
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 ProofShellCommand Source
data ProofReason Source
UserProof UserProofTechnique | Run the technique, mark Proven if succeeds |