{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}

-- |

-- Module      : OAlg.Structure.PartiallyOrdered.Proposition

-- Description : propositions on partially ordered types.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- propositions on partially ordered types.

module OAlg.Structure.PartiallyOrdered.Proposition
  (  prpErasable
  , prpSomePartiallyOrdered

  )
  where

import OAlg.Prelude

import OAlg.Data.Symbol

import OAlg.Structure.PartiallyOrdered.Definition



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

-- prpErasable -


-- | validity of a erasable lattice.

prpErasable :: (PartiallyOrdered a, Erasable a, Show a) => X a -> Statement
prpErasable :: forall a.
(PartiallyOrdered a, Erasable a, Show a) =>
X a -> Statement
prpErasable X a
xa = String -> Label
Prp String
"ErasableLattice" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (a, a) -> ((a, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (a, a)
xaa (\(a
a,a
b) -> ((a
a a -> a -> a
forall a. Erasable a => a -> a -> a
// a
b) a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
a) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
a,String
"b"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
b])
      ]
  where xaa :: X (a, a)
xaa = X a -> X a -> X (a, a)
forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xa X a
xa


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

-- prpSomePartiallyOrdered -


-- | validity of some partially ordered types.

prpSomePartiallyOrdered :: Statement
prpSomePartiallyOrdered :: Statement
prpSomePartiallyOrdered = String -> Label
Prp String
"LatticeBool" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X Bool -> Statement
forall a.
(PartiallyOrdered a, Erasable a, Show a) =>
X a -> Statement
prpErasable X Bool
xBool
      , X [Symbol] -> Statement
forall a.
(PartiallyOrdered a, Erasable a, Show a) =>
X a -> Statement
prpErasable (N -> N -> X Symbol -> X [Symbol]
forall x. N -> N -> X x -> X [x]
xTakeB N
0 N
20 (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol))
      ]