{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
module Copilot.Language.Operators.Propositional (not) where
import Prelude (($))
import Copilot.Language.Spec (Prop (..))
import qualified Copilot.Language.Operators.Boolean as B
import Copilot.Theorem
class Negatable a b where
not :: a -> b
instance Negatable (Prop Existential) (Prop Universal) where
not :: Prop Existential -> Prop Universal
not (Exists Stream Bool
p) = Stream Bool -> Prop Universal
Forall forall a b. (a -> b) -> a -> b
$ Stream Bool -> Stream Bool
B.not Stream Bool
p
instance Negatable (Prop Universal) (Prop Existential) where
not :: Prop Universal -> Prop Existential
not (Forall Stream Bool
p) = Stream Bool -> Prop Existential
Exists forall a b. (a -> b) -> a -> b
$ Stream Bool -> Stream Bool
B.not Stream Bool
p