{-# OPTIONS_GHC -O0 #-}
{-# LANGUAGE Safe #-}

-- | Augment types with invariants.

module Copilot.Theorem.TransSys.Invariants
  ( HasInvariants (..)
  , prop
  ) where

-- | Type class for types with additional invariants or contraints.
class HasInvariants a where

  invariants :: a -> [(String, Bool)]

  checkInvs :: a -> Bool
  checkInvs a
obj = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. HasInvariants a => a -> [(String, Bool)]
invariants a
obj

-- | Creates an invariant with a description.
prop :: String -> Bool -> (String, Bool)
prop :: String -> Bool -> (String, Bool)
prop = (,)