{-# LANGUAGE Safe #-}
module Copilot.Theorem.Tactics
( instantiate, assume, admit
) where
import Copilot.Theorem.Prove
import Control.Monad.Writer
instantiate :: Proof Universal -> Proof Existential
instantiate :: Proof Universal -> Proof Existential
instantiate (Proof Writer [Action] ()
p) = forall b a. Writer [Action] b -> ProofScheme a b
Proof Writer [Action] ()
p
assume :: PropRef Universal -> Proof a
assume :: forall a. PropRef Universal -> Proof a
assume (PropRef PropId
p) = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [PropId -> Action
Assume PropId
p]
admit :: Proof a
admit :: forall a. Proof a
admit = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Action
Admit]