contract-0.1.0.0

Copyright	(c) Xie Ruifeng 2020
License	AGPL-3
Maintainer	krantz.xrf@outlook.com
Stability	experimental
Portability	portable
Safe Haskell	None
Language	Haskell2010

Language.Contract.Proof

Description

Synopsis

pattern Falsified :: ThmResult
pattern Proven :: ThmResult
isFalsified :: SMTResult -> Bool
tryProve :: MonadIO m => [Type] -> [Term] -> Term -> m (Maybe ThmResult)
naiveTryProve :: (MonadFail m, MonadIO m) => [Type] -> [Term] -> Term -> m ()

Documentation

pattern Falsified :: ThmResult Source #

A falsified theorem.

pattern Proven :: ThmResult Source #

A proven theorem.

isFalsified :: SMTResult -> Bool Source #

Is this theorem falsified?

tryProve :: MonadIO m => [Type] -> [Term] -> Term -> m (Maybe ThmResult) Source #

Try prove with sbv.

naiveTryProve :: (MonadFail m, MonadIO m) => [Type] -> [Term] -> Term -> m () Source #

Use the naive theorem prover.