    {-# LANGUAGE Safe #-}

    -- | Utility functions to help write proof tactics.

    module Copilot.Theorem.Tactics
      ( instantiate, assume, admit
      ) where

    import Copilot.Theorem.Prove

    import Control.Monad.Writer

    -- | Instantiate a universal proof into an existential proof.
    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 that a property, given by reference, holds.
    assume :: PropRef Universal -> Proof a
    assume :: forall a. PropRef Universal -> Proof a
    assume (PropRef PropId
    p) = Writer [Action] () -> ProofScheme a ()
    forall b a. Writer [Action] b -> ProofScheme a b
    Proof (Writer [Action] () -> ProofScheme a ())
    -> Writer [Action] () -> ProofScheme 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]

    -- | Assume that the current goal holds.
    admit :: Proof a
    admit :: forall a. Proof a
    admit = Writer [Action] () -> ProofScheme a ()
    forall b a. Writer [Action] b -> ProofScheme a b
    Proof (Writer [Action] () -> ProofScheme a ())
    -> Writer [Action] () -> ProofScheme a ()
    forall a b. (a -> b) -> a -> b
    $ [Action] -> Writer [Action] ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Action
    Admit]