module Noether.Algebra.Actions.Compatible where
import Data.Complex
import Noether.Lemmata.Prelude
import Noether.Lemmata.TypeFu
import Noether.Algebra.Single
import Noether.Algebra.Tags
import Noether.Algebra.Actions.Acts
class CompatibleK (lr :: Side) (op :: k1) (act :: k2) a b (s :: CompatibleE)
data CompatibleE = Compatible_Acts_Semigroup
{ compatible_actor :: Type
, compatible_action :: ActsE
, compatible_actor_semigroup :: SemigroupE
}
type family CompatibleS (lr :: Side) (op :: k1) (act :: k2) (a :: Type) (b :: Type) = (r :: CompatibleE)
instance (ActsK lr act a b za, SemigroupK op a zs) =>
CompatibleK lr op act a b (Compatible_Acts_Semigroup a za zs)