Rerefined.Predicate.Logical.And

Documentation

data And l r

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

Associated Types

type PredicateName d (And l r) :: Symbol

(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

rerefineAndL :: Refined (And l r) a -> Refined l a

Take just the left predicate from an And.

rerefineAndR :: Refined (And l r) a -> Refined r a

Take just the right predicate from an And.

eliminateAndLR :: Refined (And l r) a -> Refined r (Refined l a)

Eliminate an And by applying the left predicate, then the right.

eliminateAndRL :: Refined (And l r) a -> Refined l (Refined r a)

Eliminate an And by applying the right predicate, then the left.

introduceAndLR :: Refined r (Refined l a) -> Refined (And l r) a

Introduce an And given a double-Refined. Inner is left.

introduceAndRL :: Refined l (Refined r a) -> Refined (And l r) a

Introduce an And given a double-Refined. Inner is right.