{-# 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]