{-# 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) = Writer [Action] () -> Proof Existential
forall b a. Writer [Action] b -> ProofScheme a b
Proof Writer [Action] ()
p
assume :: PropRef Universal -> Proof a
assume :: PropRef Universal -> Proof a
assume (PropRef PropId
p) = Writer [Action] () -> Proof a
forall b a. Writer [Action] b -> ProofScheme a b
Proof (Writer [Action] () -> Proof a) -> Writer [Action] () -> Proof a
forall a b. (a -> b) -> a -> b
$ [Action] -> Writer [Action] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [PropId -> Action
Assume PropId
p]
admit :: Proof a
admit :: Proof a
admit = Writer [Action] () -> Proof a
forall b a. Writer [Action] b -> ProofScheme a b
Proof (Writer [Action] () -> Proof a) -> Writer [Action] () -> Proof a
forall a b. (a -> b) -> a -> b
$ [Action] -> Writer [Action] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Action
Admit]