copilot-theorem-3.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

Prover 

Fields

data PropRef a where Source #

Constructors

PropRef :: PropId -> PropRef a 

type Proof a = ProofScheme a () Source #

data ProofScheme a b where Source #

Constructors

Proof :: Writer [Action] b -> ProofScheme a b 
Instances
Monad (ProofScheme a) Source # 
Instance details

Defined in Copilot.Theorem.Prove

Methods

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

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

return :: a0 -> ProofScheme a a0 #

fail :: String -> ProofScheme a a0 #

Functor (ProofScheme a) Source # 
Instance details

Defined in Copilot.Theorem.Prove

Methods

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

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

Applicative (ProofScheme a) Source # 
Instance details

Defined in Copilot.Theorem.Prove

Methods

pure :: a0 -> ProofScheme a a0 #

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

liftA2 :: (a0 -> b -> c) -> ProofScheme a a0 -> ProofScheme a b -> ProofScheme a c #

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

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

data Action where Source #

Constructors

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

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