| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Copilot.Theorem.Prove
Documentation
Constructors
| Prover | |
Fields
| |
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 # | |
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 # | |
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 # | |
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 Existential Source #