{-# LANGUAGE NoImplicitPrelude #-}

-- |

-- Module      : OAlg.Proposition

-- Description : validation of this package.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- validation of this package.

module OAlg.Proposition
  ( prpOAlgBase
  ) where

import OAlg.Prelude
import OAlg.Structure.Proposition
import OAlg.Hom.Proposition
import OAlg.Limes.Proposition

import OAlg.Entity.Product
import OAlg.Entity.Diagram.Proposition
import OAlg.Entity.Matrix
import OAlg.Entity.Sequence

--------------------------------------------------------------------------------

-- prpOAlgBase -


-- | Validation of the basic entities of the package oalg-base.

prpOAlgBase :: Statement
prpOAlgBase :: Statement
prpOAlgBase = String -> Label
Prp String
"OAlgBase"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ String -> Label
Label String
"logic" Label -> Statement -> Statement
:<=>:
                [Statement] -> Statement
And [ Statement
prpBool
                    , Statement
prpValidTautologies
                    , Statement
prpStatement
                    ]
            , Statement
prpStructure
            , String -> Label
Label String
"HomDisjOp" Label -> Statement -> Statement
:<=>: Statement
prpHomDisjOp
            , String -> Label
Label String
"Product" Label -> Statement -> Statement
:<=>: Statement
prpOrtProductZOrntSymbol
            , String -> Label
Label String
"Diagram" Label -> Statement -> Statement
:<=>: Statement
prpDiagramOrntSymbol
            , String -> Label
Label String
"Limes"   Label -> Statement -> Statement
:<=>: N -> Statement
prpLimitsOrntSymbol N
5
            , String -> Label
Label String
"Permutation" Label -> Statement -> Statement
:<=>: Statement
prpPermutation
            , String -> Label
Label String
"Matrix"  Label -> Statement -> Statement
:<=>: Statement
prpMatrixZ
            , String -> Label
Label String
"Vector"  Label -> Statement -> Statement
:<=>: N -> N -> Statement
prpRepMatrixZ N
8 N
15
            , Statement
prpPSequence
            , Statement
prpFSequence
            ]