Safe Haskell	None
Language	GHC2021

Rerefined.Predicate.Logical

Description

Logical predicates.

Pretty predicates use infix propositional operators. This is chosen for consistency. I'm not really sure which I prefer over all, perhaps best would be to mix and match. Please let the maintainers know if you have a better idea.

Synopsis

data And (l :: k) (r :: k1)
data Iff (l :: k) (r :: k1)
data If (l :: k) (r :: k1)
data Nand (l :: k) (r :: k1)
data Nor (l :: k) (r :: k1)
data Not (p :: k)
data Or (l :: k) (r :: k1)
data Xor (l :: k) (r :: k1)

Documentation

data And (l :: k) (r :: k1) Source #

Logical conjunction. Also AND logic gate.

Instances

Instances details

(Predicate l, Predicate r) => Predicate (And l r :: Type) Source #	Precedence of 3 (matching `&&`).
Instance details Defined in Rerefined.Predicate.Logical.And
(Refine l a, Refine r a, KnownPredicateName (And l r)) => Refine (And l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.And Methods validate :: Proxy# (And l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (And l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.And type PredicateName d (And l r :: Type) = PredicateNameBOp " \8743 " 3 d l r

data Iff (l :: k) (r :: k1) Source #

Logical biconditional ("if and only if"). Also the XNOR logic gate, or equivalence (loosely).

Instances

Instances details

(Predicate l, Predicate r) => Predicate (Iff l r :: Type) Source #	Precedence of 4 (matching `==`).
Instance details Defined in Rerefined.Predicate.Logical.Iff
(Refine l a, Refine r a, KnownPredicateName (Iff l r)) => Refine (Iff l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Iff Methods validate :: Proxy# (Iff l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (Iff l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Iff type PredicateName d (Iff l r :: Type) = PredicateNameBOp " \8596 " 4 d l r

data If (l :: k) (r :: k1) Source #

Logical implication. "If l then r".

Instances

Instances details

(Predicate l, Predicate r) => Predicate (If l r :: Type) Source #	Precedence of 4 (matching `==`).
Instance details Defined in Rerefined.Predicate.Logical.If
(Refine l a, Refine r a, KnownPredicateName (If l r)) => Refine (If l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.If Methods validate :: Proxy# (If l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (If l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.If type PredicateName d (If l r :: Type) = PredicateNameBOp " \8594 " 4 d l r

data Nand (l :: k) (r :: k1) Source #

NAND logic gate. Also called the Sheffer stroke, or non-conjunction.

Instances

Instances details

(Predicate l, Predicate r) => Predicate (Nand l r :: Type) Source #	Precedence of 3 (matching `&&`).
Instance details Defined in Rerefined.Predicate.Logical.Nand
(Refine l a, Refine r a, KnownPredicateName (Nand l r)) => Refine (Nand l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Nand Methods validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (Nand l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Nand type PredicateName d (Nand l r :: Type) = PredicateNameBOp " \8892 " 3 d l r

data Nor (l :: k) (r :: k1) Source #

NOR logic gate. Also called non-disjunction, or joint denial.

Instances

Instances details

(Predicate l, Predicate r) => Predicate (Nor l r :: Type) Source #	Precedence of 2 (matching `\|\|`).
Instance details Defined in Rerefined.Predicate.Logical.Nor
(Refine l a, Refine r a, KnownPredicateName (Nor l r)) => Refine (Nor l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Nor Methods validate :: Proxy# (Nor l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (Nor l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Nor type PredicateName d (Nor l r :: Type) = PredicateNameBOp " \8893 " 2 d l r

data Not (p :: k) Source #

Logical negation. Also NOT logic gate, or logical complement.

Instances

Instances details

Predicate p => Predicate (Not p :: Type) Source #	Precedence of 9 (one below function application).
Instance details Defined in Rerefined.Predicate.Logical.Not
(Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Not Methods validate :: Proxy# (Not p) -> a -> Maybe RefineFailure Source #
type PredicateName d (Not p :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Not type PredicateName d (Not p :: Type) = ShowParen (d > 9) ("\172 " ++ PredicateName 10 p)

data Or (l :: k) (r :: k1) Source #

Logical disjunction. Also OR logic gate.

Instances

Instances details

(Predicate l, Predicate r) => Predicate (Or l r :: Type) Source #	Precedence of 2 (matching `\|\|`).
Instance details Defined in Rerefined.Predicate.Logical.Or
(Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Or Methods validate :: Proxy# (Or l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (Or l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Or type PredicateName d (Or l r :: Type) = PredicateNameBOp " \8744 " 2 d l r

data Xor (l :: k) (r :: k1) Source #

Logical exclusive disjunction. Also XOR logic gate.

Instances

Instances details

(Predicate l, Predicate r) => Predicate (Xor l r :: Type) Source #	Precedence of 4 (matching `==`).
Instance details Defined in Rerefined.Predicate.Logical.Xor
(Refine l a, Refine r a, KnownPredicateName (Xor l r)) => Refine (Xor l r :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Logical.Xor Methods validate :: Proxy# (Xor l r) -> a -> Maybe RefineFailure Source #
type PredicateName d (Xor l r :: Type) Source #
Instance details Defined in Rerefined.Predicate.Logical.Xor type PredicateName d (Xor l r :: Type) = PredicateNameBOp " \8853 " 4 d l r