| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Rerefined.Predicate.Logical.And
Synopsis
- data And (l :: k) (r :: k1)
- rerefineAndL :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined l a
- rerefineAndR :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined r a
- eliminateAndLR :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined r (Refined l a)
- eliminateAndRL :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined l (Refined r a)
- introduceAndLR :: forall {k1} {k2} (r :: k1) (l :: k2) a. Refined r (Refined l a) -> Refined (And l r) a
- introduceAndRL :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined l (Refined r a) -> Refined (And l r) a
Documentation
data And (l :: k) (r :: k1) Source #
Logical conjunction. Also AND logic gate.
Instances
| (Predicate l, Predicate r) => Predicate (And l r :: Type) Source # | 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 Source # | |
Defined in Rerefined.Predicate.Logical.And | |
| type PredicateName d (And l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.And | |
rerefineAndL :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined l a Source #
Take just the left predicate from an And.
rerefineAndR :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined r a Source #
Take just the right predicate from an And.
eliminateAndLR :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined r (Refined l a) Source #
Eliminate an And by applying the left predicate, then the right.
eliminateAndRL :: forall {k1} {k2} (l :: k1) (r :: k2) a. Refined (And l r) a -> Refined l (Refined r a) Source #
Eliminate an And by applying the right predicate, then the left.