instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
-- Typing
+instance NameTyOf Ratio where
+ nameTyOf _c = ["Ratio"] `Mod` "Ratio"
instance FixityOf Ratio
instance ClassInstancesFor Ratio where
- proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
+ proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a)
| Just HRefl <- proj_ConstKiTy @_ @Ratio c
= case () of
_ | Just Refl <- proj_Const @Eq q
- , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Show q
- , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Real q
, Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
| Just Refl <- proj_Const @Ord q
-- Compiling
instance Gram_Term_AtomsFor src ss g Ratio
-instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where
+instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
moduleFor = ["Ratio"] `moduleWhere`
[ "ratio" := teRatio
, "numerator" := teRatio_numerator