import Language.Symantic.Lib.MonoFunctor (e1, famElement)
-- * Class 'Sym_SemiSequence'
-type instance Sym (Proxy SemiSequence) = Sym_SemiSequence
+type instance Sym SemiSequence = Sym_SemiSequence
class Sym_SemiSequence term where
intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
-- Typing
+instance NameTyOf SemiSequence where
+ nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
instance FixityOf SemiSequence
instance ClassInstancesFor SemiSequence
instance TypeInstancesFor SemiSequence
-- Compiling
instance Gram_Term_AtomsFor src ss g SemiSequence
-instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where
- moduleFor _s = ["SemiSequence"] `moduleWhere`
+instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
+ moduleFor = ["SemiSequence"] `moduleWhere`
[ "intersperse" := teSemiSequence_intersperse
, "cons" := teSemiSequence_cons
, "snoc" := teSemiSequence_snoc
tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
-s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>
+s0 :: Source src => LenInj vs => KindInj (K s) =>
Type src (Proxy s ': vs) s
s0 = tyVar "s" varZ
teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
-- * Class 'Sym_IsSequence'
-type instance Sym (Proxy IsSequence) = Sym_IsSequence
+type instance Sym IsSequence = Sym_IsSequence
class Sym_IsSequence term where
filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
-- Typing
+instance NameTyOf IsSequence where
+ nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
instance FixityOf IsSequence
instance ClassInstancesFor IsSequence
instance TypeInstancesFor IsSequence
-- Compiling
instance Gram_Term_AtomsFor src ss g IsSequence
-instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where
- moduleFor _s = ["IsSequence"] `moduleWhere`
+instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
+ moduleFor = ["IsSequence"] `moduleWhere`
[ "filter" := teIsSequence_filter
]