Copyright | (c) Erich Gut |
---|---|
License | BSD3 |
Maintainer | zerich.gut@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
propositions about Distributive
structure.
Synopsis
- prpDst :: Distributive d => XDst d -> Statement
- data XDst d = XDst (X (DstRootSide LeftSide d)) (X (DstSide LeftSide d)) (X (DstRootSide RightSide d)) (X (DstSide RightSide d))
- prpDst1 :: Distributive d => X (DstRootSide LeftSide d) -> Statement
- prpDst2 :: Distributive d => X (DstSide LeftSide d) -> Statement
- prpDst3 :: Distributive d => X (DstRootSide RightSide d) -> Statement
- prpDst4 :: Distributive d => X (DstSide RightSide d) -> Statement
- data DstRootSide (s :: Side) d where
- LDstRoot :: Root d -> d -> DstRootSide LeftSide d
- RDstRoot :: d -> Root d -> DstRootSide RightSide d
- data DstSide (s :: Side) d where
- class XStandardDst d where
- xStandardDst :: XDst d
- xDstStalkStartEnd :: Distributive m => XStalk m -> XOrtSite From m -> XOrtSite To m -> XDst m
- xDstTtl :: Singleton (Root m) => X m -> XDst m
- xDstOrnt :: Entity p => X p -> XDst (Orientation p)
- xoDst :: Distributive d => XOrtOrientation d -> XOrtSite From d -> XOrtSite To d -> XDst d
- dstDst :: Distributive d => Int -> XDst d -> IO ()
Distributive
prpDst :: Distributive d => XDst d -> Statement Source #
validity for the Distributive
structure of the type a
.
random variable for validating Distributive
structures.
prpDst1 :: Distributive d => X (DstRootSide LeftSide d) -> Statement Source #
validity according to OAlg.Structure.Distributive.
prpDst2 :: Distributive d => X (DstSide LeftSide d) -> Statement Source #
validity according to OAlg.Structure.Distributive.
prpDst3 :: Distributive d => X (DstRootSide RightSide d) -> Statement Source #
validity according to OAlg.Structure.Distributive.
prpDst4 :: Distributive d => X (DstSide RightSide d) -> Statement Source #
validity according to OAlg.Structure.Distributive.
data DstRootSide (s :: Side) d where Source #
predicate for a root and a factor at the root.
Properties Let p
be in
for a DstRootSide
s dDistributive
structure d
,
then holds:
LDstRoot :: Root d -> d -> DstRootSide LeftSide d | |
RDstRoot :: d -> Root d -> DstRootSide RightSide d |
Instances
Distributive d => Show (DstRootSide s d) Source # | |
Defined in OAlg.Structure.Distributive.Proposition showsPrec :: Int -> DstRootSide s d -> ShowS # show :: DstRootSide s d -> String # showList :: [DstRootSide s d] -> ShowS # | |
Distributive d => Dualisable (DstRootSide 'RightSide d) Source # | |
Defined in OAlg.Structure.Distributive.Proposition toDual :: DstRootSide 'RightSide d -> Dual (DstRootSide 'RightSide d) Source # fromDual :: Dual (DstRootSide 'RightSide d) -> DstRootSide 'RightSide d Source # | |
Distributive d => Validable (DstRootSide s d) Source # | |
Defined in OAlg.Structure.Distributive.Proposition valid :: DstRootSide s d -> Statement Source # | |
type Dual (DstRootSide s d :: Type) Source # | |
Defined in OAlg.Structure.Distributive.Proposition |
data DstSide (s :: Side) d where Source #
predicate for two addable summands together with a matching factor.
Properties Let p
be in
for a DstSide
s dDistributive
structure, then holds:
X
class XStandardDst d where Source #
standard random variable for Distributive
structures.
xStandardDst :: XDst d Source #
Instances
XStandardDst N Source # | |
Defined in OAlg.Structure.Distributive.Proposition xStandardDst :: XDst N Source # | |
XStandardDst Q Source # | |
Defined in OAlg.Structure.Distributive.Proposition xStandardDst :: XDst Q Source # | |
XStandardDst Z Source # | |
Defined in OAlg.Structure.Distributive.Proposition xStandardDst :: XDst Z Source # | |
(Entity p, XStandard p) => XStandardDst (Orientation p) Source # | |
Defined in OAlg.Structure.Distributive.Proposition xStandardDst :: XDst (Orientation p) Source # |
xDstStalkStartEnd :: Distributive m => XStalk m -> XOrtSite From m -> XOrtSite To m -> XDst m Source #
the induced random variable for Distributive
structures.
Total
xDstTtl :: Singleton (Root m) => X m -> XDst m Source #
random variable to validate Total
Distributive
structures.
Orientation
xDstOrnt :: Entity p => X p -> XDst (Orientation p) Source #
random variable for the Distributive
structure of
.Orientation
p
Oriented Direction
xoDst :: Distributive d => XOrtOrientation d -> XOrtSite From d -> XOrtSite To d -> XDst d Source #
the induced random variable for Distributive
structures.