| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
OAlg.Structure.Additive.Proposition
Description
propositions on Additive structures.
Synopsis
- relIsZero :: Additive a => a -> Statement
- prpAdd :: Additive a => XAdd a -> Statement
- prpAdd1 :: Additive a => p a -> X (Root a) -> Statement
- prpAdd2 :: Additive a => X (a, a) -> Statement
- prpAdd2_1 :: Additive a => Adbl2 a -> Statement
- prpAdd2_2 :: Additive a => a -> a -> Statement
- prpAdd3 :: Additive a => X (Adbl2 a) -> Statement
- prpAdd4 :: Additive a => X a -> Statement
- prpAdd5 :: Additive a => X (Adbl3 a) -> Statement
- prpAdd6 :: Additive a => X N -> X a -> Statement
- prpAbl :: Abelian a => XAbl a -> Statement
- prpAbl1 :: Abelian a => X a -> Statement
- prpAbl2 :: Abelian a => X a -> Statement
- prpAbl3 :: Abelian a => X (a, a) -> Statement
- prpAbl3_1 :: Abelian a => Adbl2 a -> Statement
- prpAbl3_2 :: Abelian a => a -> a -> Statement
- prpAbl4 :: Abelian a => X (Adbl2 a) -> Statement
- prpAbl5 :: Abelian a => X Z -> X a -> Statement
- data XAdd a = XAdd (X N) (X (Root a)) (X a) (X (Adbl2 a)) (X (Adbl3 a))
- data Adbl2 a = Adbl2 a a
- data Adbl3 a = Adbl3 a a a
- class XStandardAdd a where
- xStandardAdd :: XAdd a
- data XAbl a = XAbl (X Z) (X a) (X (Adbl2 a))
- xAddTtl :: Singleton (Root a) => X N -> X a -> XAdd a
- xoAdd :: FibredOriented a => X N -> XOrtOrientation a -> XAdd a
- xoRoot :: FibredOriented a => XOrtOrientation a -> X (Root a)
- xoAdbl2 :: FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
- xoAdbl3 :: FibredOriented a => XOrtOrientation a -> X (Adbl3 a)
- xoAbl :: FibredOriented a => X Z -> XOrtOrientation a -> XAbl a
- xoFbr :: XOrtOrientation f -> XFbr f
- xAddOrnt :: Entity p => X N -> X p -> XAdd (Orientation p)
- xAddStalk :: Additive a => XStalk a -> X N -> XAdd a
- xStalkAdbl2 :: Additive a => XStalk a -> Root a -> X (Adbl2 a)
- xStalkAdbl3 :: Additive a => XStalk a -> Root a -> X (Adbl3 a)
Additive
prpAdd1 :: Additive a => p a -> X (Root a) -> Statement Source #
validtiy of root according to OAlg.Structure.Additive.Definition.
prpAdd2 :: Additive a => X (a, a) -> Statement Source #
validtiy of two summands according to OAlg.Structure.Additive.Definition.
prpAdd2_1 :: Additive a => Adbl2 a -> Statement Source #
validity of + for two addable summands according to
OAlg.Structure.Additive.Definition.
prpAdd2_2 :: Additive a => a -> a -> Statement Source #
validity of + for two not addable summands according to
OAlg.Structure.Additive.Definition.
prpAdd3 :: Additive a => X (Adbl2 a) -> Statement Source #
validtiy of two adable summands according to OAlg.Structure.Additive.Definition.
prpAdd4 :: Additive a => X a -> Statement Source #
validtiy according to OAlg.Structure.Additive.Definition.
prpAdd5 :: Additive a => X (Adbl3 a) -> Statement Source #
validtiy of three adable summands according to OAlg.Structure.Additive.Definition.
prpAdd6 :: Additive a => X N -> X a -> Statement Source #
validity of ntimes according to OAlg.Structure.Additive.Definition.
Abelian
prpAbl1 :: Abelian a => X a -> Statement Source #
validity according to OAlg.Structure.Additive.Definition.
prpAbl2 :: Abelian a => X a -> Statement Source #
validity according to OAlg.Structure.Additive.Definition.
prpAbl3 :: Abelian a => X (a, a) -> Statement Source #
validity of two summands according to OAlg.Structure.Additive.Definition.
prpAbl3_1 :: Abelian a => Adbl2 a -> Statement Source #
validity of - for two addable summands according to
OAlg.Structure.Additive.Definition.
prpAbl3_2 :: Abelian a => a -> a -> Statement Source #
validity of - for two not addable summands according to
OAlg.Structure.Additive.Definition.
prpAbl4 :: Abelian a => X (Adbl2 a) -> Statement Source #
validity of two summands according to OAlg.Structure.Additive.Definition.
prpAbl5 :: Abelian a => X Z -> X a -> Statement Source #
validity of two summands according to OAlg.Structure.Additive.Definition.
X
Additive
random variable for validating Additive structures.
predicate for two addable summands.
Constructors
| Adbl2 a a |
predicate for three addable summands.
Constructors
| Adbl3 a a a |
class XStandardAdd a where Source #
standard random variable for Additive structures.
Methods
xStandardAdd :: XAdd a Source #
Instances
| XStandardAdd N Source # | |
Defined in OAlg.Structure.Additive.Proposition Methods xStandardAdd :: XAdd N Source # | |
| XStandardAdd Q Source # | |
Defined in OAlg.Structure.Additive.Proposition Methods xStandardAdd :: XAdd Q Source # | |
| XStandardAdd Z Source # | |
Defined in OAlg.Structure.Additive.Proposition Methods xStandardAdd :: XAdd Z Source # | |
| (Entity p, XStandard p) => XStandardAdd (Orientation p) Source # | |
Defined in OAlg.Structure.Additive.Proposition Methods xStandardAdd :: XAdd (Orientation p) Source # | |
Abelian
random variable for validating Abelian structures.
Total
xAddTtl :: Singleton (Root a) => X N -> X a -> XAdd a Source #
random variable for total Additive structures.
Direction
xoAdd :: FibredOriented a => X N -> XOrtOrientation a -> XAdd a Source #
xoRoot :: FibredOriented a => XOrtOrientation a -> X (Root a) Source #
the induced random variables for roots.
xoAdbl2 :: FibredOriented a => XOrtOrientation a -> X (Adbl2 a) Source #
the induced random variable for two addable summands.
xoAdbl3 :: FibredOriented a => XOrtOrientation a -> X (Adbl3 a) Source #
the induced random variable for three addable summands.
xoAbl :: FibredOriented a => X Z -> XOrtOrientation a -> XAbl a Source #
xoFbr :: XOrtOrientation f -> XFbr f Source #
the associated random variable for validating Fibred structures.
Orientation
xAddOrnt :: Entity p => X N -> X p -> XAdd (Orientation p) Source #
random variable for the Additive structure of Orientation p
Stalk
xAddStalk :: Additive a => XStalk a -> X N -> XAdd a Source #
random variable for Additive structure.