copilot-theorem-2.2.0: 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

forall r . Prover 

Fields

proverName :: String
 
startProver :: Spec -> IO r
 
askProver :: r -> [PropId] -> [PropId] -> IO Output
 
closeProver :: r -> IO ()
 

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

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