{-# LANGUAGE Safe #-}

-- | Highly automated proof techniques are a necessary step for the widespread
-- adoption of formal methods in the software industry. Moreover, it could
-- provide a partial answer to one of its main issue which is scalability.
--
-- Copilot-theorem is a Copilot library aimed at checking automatically some
-- safety properties on Copilot programs. It includes:
--
-- * A prover producing native inputs for the Kind2 model checker.
--
-- * A What4 backend that uses SMT solvers to prove safety properties.

module Copilot.Theorem
  ( module X
  , Proof
  , PropId, PropRef
  , Universal, Existential
  ) where

import Copilot.Theorem.Tactics as X
import Copilot.Theorem.Prove