rerefined-0.5.1: Refinement types, again
Safe HaskellSafe-Inferred
LanguageGHC2021

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

Documentation

data And l r 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

Associated Types

type PredicateName d (And l r) :: Symbol Source #

(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 r 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

Associated Types

type PredicateName d (Iff l r) :: Symbol Source #

(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 r 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

Associated Types

type PredicateName d (If l r) :: Symbol Source #

(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 r 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

Associated Types

type PredicateName d (Nand l r) :: Symbol Source #

(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 r 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

Associated Types

type PredicateName d (Nor l r) :: Symbol Source #

(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 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

Associated Types

type PredicateName d (Not p) :: Symbol Source #

(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 r Source #

Logical disjunction. Also OR logic gate.

Instances

Instances details
ReifyRelOp GTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE :: Symbol Source #

Methods

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

ReifyRelOp LTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE :: Symbol Source #

Methods

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

ReifyRelOp NEQ Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ :: Symbol Source #

Methods

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

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

Precedence of 2 (matching ||).

Instance details

Defined in Rerefined.Predicate.Logical.Or

Associated Types

type PredicateName d (Or l r) :: Symbol Source #

ReifyRelOp (Or 'EQ 'GT) Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT) :: Symbol Source #

Methods

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

ReifyRelOp (Or 'EQ 'LT) Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT) :: Symbol Source #

Methods

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

ReifyRelOp (Or 'GT 'LT) Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT) :: Symbol Source #

Methods

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

(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 ShowRelOp GTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="
type ShowRelOp LTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="
type ShowRelOp NEQ Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="
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
type ShowRelOp (Or 'EQ 'GT) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Internal

data Xor l r 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

Associated Types

type PredicateName d (Xor l r) :: Symbol Source #

(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