Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Structure.Distributive.Proposition

Contents

Distributive
X
Tools

Description

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))
data DstX
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 :: forall d. Root d -> d -> DstRootSide 'LeftSide d
- RDstRoot :: forall d. d -> Root d -> DstRootSide 'RightSide d
data DstSide (s :: Side) d where
- LDst :: forall d. (d, d) -> d -> DstSide 'LeftSide d
- RDst :: forall d. d -> (d, d) -> DstSide 'RightSide d
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.

data XDst d Source #

random variable for validating Distributive structures.

Constructors

XDst (X (DstRootSide 'LeftSide d)) (X (DstSide 'LeftSide d)) (X (DstRootSide 'RightSide d)) (X (DstSide 'RightSide d))

data DstX Source #

type index for Distributive structures admitting XStandardOrtOrientation.

Instances

Instances details

TransformableAdd DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableType DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableDst DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableFbr DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableFbrOrt DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableMlt DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableOrt DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableOp DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
Transformable DstX Add Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Add x Source #
Transformable DstX Typ Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Typ x Source #
Transformable DstX Dst Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Dst x Source #
Transformable DstX Fbr Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Fbr x Source #
Transformable DstX FbrOrt Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct FbrOrt x Source #
Transformable DstX Mlt Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Mlt x Source #
Transformable DstX Ort Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Ort x Source #
Transformable DstX Type Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tau :: Struct DstX x -> Struct Type x Source #
TransformableGRefl Matrix DstX Source #
Instance details Defined in OAlg.Entity.Matrix.Definition
TransformableGRefl Op DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition
TransformableG Matrix DstX DstX Source #
Instance details Defined in OAlg.Entity.Matrix.Definition Methods tauG :: Struct DstX x -> Struct DstX (Matrix x) Source #
TransformableG Op DstX DstX Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods tauG :: Struct DstX x -> Struct DstX (Op x) Source #
type Structure DstX x Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition type Structure DstX x = (Distributive x, XStandardOrtOrientation x)

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 DstRootSide s d for a Distributive structure d, then holds:

If p matches LDstRoot r f then holds: start r == end f.
If p matches RDstRoot f r then holds: start f == end r.

Constructors

LDstRoot :: forall d. Root d -> d -> DstRootSide 'LeftSide d
RDstRoot :: forall d. d -> Root d -> DstRootSide 'RightSide d

Instances

Instances details

Distributive d => Show (DstRootSide s d) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods showsPrec :: Int -> DstRootSide s d -> ShowS # show :: DstRootSide s d -> String # showList :: [DstRootSide s d] -> ShowS #
Distributive d => Dualisable (DstRootSide 'RightSide d) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods 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 #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods valid :: DstRootSide s d -> Statement Source #
type Dual (DstRootSide s d :: Type) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition type Dual (DstRootSide s d :: Type) = DstRootSide (Dual s) (Op d)

data DstSide (s :: Side) d where Source #

predicate for two addable summands together with a matching factor.

Properties Let p be in DstSide s d for a Distributive structure, then holds:

If p matches LDst (a,b) g then holds:
1. root a == root b.
2. start a == end g.
If p matches RDst f (a,b) then holds:
1. root a == root b.
2. start f == end a.

Constructors

LDst :: forall d. (d, d) -> d -> DstSide 'LeftSide d
RDst :: forall d. d -> (d, d) -> DstSide 'RightSide d

Instances

Instances details

Distributive d => Show (DstSide s d) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods showsPrec :: Int -> DstSide s d -> ShowS # show :: DstSide s d -> String # showList :: [DstSide s d] -> ShowS #
Distributive d => Dualisable (DstSide 'RightSide d) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods toDual :: DstSide 'RightSide d -> Dual (DstSide 'RightSide d) Source # fromDual :: Dual (DstSide 'RightSide d) -> DstSide 'RightSide d Source #
Distributive d => Validable (DstSide s d) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods valid :: DstSide s d -> Statement Source #
type Dual (DstSide s d :: Type) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition type Dual (DstSide s d :: Type) = DstSide (Dual s) (Op d)

X

class XStandardDst d where Source #

standard random variable for Distributive structures.

Methods

xStandardDst :: XDst d Source #

Instances

Instances details

XStandardDst N Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods xStandardDst :: XDst N Source #
XStandardDst Q Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods xStandardDst :: XDst Q Source #
XStandardDst Z Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods xStandardDst :: XDst Z Source #
XStandardDst x => XStandardDst (Id x) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods xStandardDst :: XDst (Id x) Source #
(FibredOriented x, XStandardDst x) => XStandardDst (Op x) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods xStandardDst :: XDst (Op x) Source #
(Entity p, XStandard p) => XStandardDst (Orientation p) Source #
Instance details Defined in OAlg.Structure.Distributive.Proposition Methods 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.

Tools

dstDst :: Distributive d => Int -> XDst d -> IO () Source #

distribution of XDst d.