Copilot.Theorem.Prove

Documentation

data Output

Constructors

Output Status [String]

data Status

Constructors

Sat

Valid

Invalid

Unknown

Error

data Prover

Constructors

Prover

Fields

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

type PropId = String

data PropRef a where

Constructors

PropRef :: PropId -> PropRef a

type Proof a = ProofScheme a ()

type UProof = Writer [Action] ()

data ProofScheme a b where

Constructors

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

Instances

Monad (ProofScheme a)

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)

Methods

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

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

Applicative (ProofScheme a)

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

Constructors

Check :: Prover -> Action

Assume :: PropId -> Action

Admit :: Action

data Universal

data Existential

check :: Prover -> Proof a

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

combine :: Prover -> Prover -> Prover