{-# OPTIONS_GHC -O0 #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Invariants
( HasInvariants (..)
, prop
) where
class HasInvariants a where
invariants :: a -> [(String, Bool)]
checkInvs :: a -> Bool
checkInvs obj :: 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
prop :: String -> Bool -> (String, Bool)
prop :: String -> Bool -> (String, Bool)
prop = (,)