    {-# 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 = ((String, Bool) -> Bool) -> [(String, Bool)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (String, Bool) -> Bool
    forall a b. (a, b) -> b
    snd ([(String, Bool)] -> Bool) -> [(String, Bool)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ a -> [(String, Bool)]
    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 = (,)