copilot-theorem-2.2.1: k-induction for Copilot.

Safe HaskellSafe
LanguageHaskell2010

Copilot.Theorem.Prove

Documentation

data Output Source #

Constructors

Output Status [String] 

data Status Source #

Constructors

Sat 
Valid 
Invalid 
Unknown 
Error 

data Prover Source #

Constructors

Prover 

Fields

type PropId = String Source #

data PropRef a where Source #

Constructors

PropRef :: PropId -> PropRef a 

type Proof a = ProofScheme a () Source #

type UProof = Writer [Action] () Source #

data ProofScheme a b where Source #

Constructors

Proof :: Writer [Action] b -> ProofScheme a b 

Instances

Monad (ProofScheme a) Source # 

Methods

(>>=) :: ProofScheme a a -> (a -> ProofScheme a b) -> ProofScheme a b #

(>>) :: ProofScheme a a -> ProofScheme a b -> ProofScheme a b #

return :: a -> ProofScheme a a #

fail :: String -> ProofScheme a a #

Functor (ProofScheme a) Source # 

Methods

fmap :: (a -> b) -> ProofScheme a a -> ProofScheme a b #

(<$) :: a -> ProofScheme a b -> ProofScheme a a #

Applicative (ProofScheme a) Source # 

Methods

pure :: a -> ProofScheme a a #

(<*>) :: ProofScheme a (a -> b) -> ProofScheme a a -> ProofScheme a b #

(*>) :: ProofScheme a a -> ProofScheme a b -> ProofScheme a b #

(<*) :: ProofScheme a a -> ProofScheme a b -> ProofScheme a a #

data Action where Source #

Constructors

Check :: Prover -> Action 
Assume :: PropId -> Action 
Admit :: Action 

data Universal Source #

data Existential Source #

check :: Prover -> Proof a Source #

prove :: Spec -> PropId -> UProof -> IO Bool Source #

combine :: Prover -> Prover -> Prover Source #