{-# LANGUAGE Safe #-}

-- | Each prover first translates the Copilot specification into an
-- intermediate representation best suited for model checking.
--
-- This module and the ones in the same namespace implement the IL format. A
-- Copilot program is translated into a list of quantifier-free equations over
-- integer sequences, implicitly universally quantified by a free variable n.
-- Each sequence roughly corresponds to a stream.

module Copilot.Theorem.IL (module X) where

import Copilot.Theorem.IL.Spec as X
import Copilot.Theorem.IL.Translate as X
import Copilot.Theorem.IL.Transform as X
import Copilot.Theorem.IL.PrettyPrint as X