Rerefined.Predicate.Logical

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.

Documentation

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

Logical conjunction. Also AND logic gate.

Instances

(Predicate l, Predicate r) => Predicate (And l r :: Type)

Precedence of 3 (matching &&).

Defined in Rerefined.Predicate.Logical.And

(Refine l a, Refine r a, KnownPredicateName (And l r)) => Refine (And l r :: Type) a

Defined in Rerefined.Predicate.Logical.And

Methods

validate :: Proxy# (And l r) -> a -> Maybe RefineFailure

type PredicateName d (And l r :: Type)

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)

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

Instances

(Predicate l, Predicate r) => Predicate (Iff l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.Iff

(Refine l a, Refine r a, KnownPredicateName (Iff l r)) => Refine (Iff l r :: Type) a

Defined in Rerefined.Predicate.Logical.Iff

Methods

validate :: Proxy# (Iff l r) -> a -> Maybe RefineFailure

type PredicateName d (Iff l r :: Type)

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)

Logical implication. "If l then r".

Instances

(Predicate l, Predicate r) => Predicate (If l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.If

(Refine l a, Refine r a, KnownPredicateName (If l r)) => Refine (If l r :: Type) a

Defined in Rerefined.Predicate.Logical.If

Methods

validate :: Proxy# (If l r) -> a -> Maybe RefineFailure

type PredicateName d (If l r :: Type)

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)

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

Instances

(Predicate l, Predicate r) => Predicate (Nand l r :: Type)

Precedence of 3 (matching &&).

Defined in Rerefined.Predicate.Logical.Nand

(Refine l a, Refine r a, KnownPredicateName (Nand l r)) => Refine (Nand l r :: Type) a

Defined in Rerefined.Predicate.Logical.Nand

Methods

validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure

type PredicateName d (Nand l r :: Type)

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)

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

Instances

(Predicate l, Predicate r) => Predicate (Nor l r :: Type)

Precedence of 2 (matching ||).

Defined in Rerefined.Predicate.Logical.Nor

(Refine l a, Refine r a, KnownPredicateName (Nor l r)) => Refine (Nor l r :: Type) a

Defined in Rerefined.Predicate.Logical.Nor

Methods

validate :: Proxy# (Nor l r) -> a -> Maybe RefineFailure

type PredicateName d (Nor l r :: Type)

Defined in Rerefined.Predicate.Logical.Nor

type PredicateName d (Nor l r :: Type) = PredicateNameBOp " \8893 " 2 d l r

data Not (p :: k)

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

Instances

Predicate p => Predicate (Not p :: Type)

Precedence of 9 (one below function application).

Defined in Rerefined.Predicate.Logical.Not

(Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a

Defined in Rerefined.Predicate.Logical.Not

Methods

validate :: Proxy# (Not p) -> a -> Maybe RefineFailure

type PredicateName d (Not p :: Type)

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)

Logical disjunction. Also OR logic gate.

Instances

ReifyRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Predicate l, Predicate r) => Predicate (Or l r :: Type)

Precedence of 2 (matching ||).

Defined in Rerefined.Predicate.Logical.Or

ReifyRelOp (Or 'EQ 'GT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'EQ 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'GT 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a

Defined in Rerefined.Predicate.Logical.Or

Methods

validate :: Proxy# (Or l r) -> a -> Maybe RefineFailure

type ShowRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="

type ShowRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="

type ShowRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="

type PredicateName d (Or l r :: Type)

Defined in Rerefined.Predicate.Logical.Or

type PredicateName d (Or l r :: Type) = PredicateNameBOp " \8744 " 2 d l r

type ShowRelOp (Or 'EQ 'GT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

type ShowRelOp (Or 'EQ 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

type ShowRelOp (Or 'GT 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

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

Logical exclusive disjunction. Also XOR logic gate.

Instances

(Predicate l, Predicate r) => Predicate (Xor l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.Xor

(Refine l a, Refine r a, KnownPredicateName (Xor l r)) => Refine (Xor l r :: Type) a

Defined in Rerefined.Predicate.Logical.Xor

Methods

validate :: Proxy# (Xor l r) -> a -> Maybe RefineFailure

type PredicateName d (Xor l r :: Type)

Defined in Rerefined.Predicate.Logical.Xor

type PredicateName d (Xor l r :: Type) = PredicateNameBOp " \8853 " 4 d l r