rerefined-0.8.0: Refinement types, again
Safe HaskellNone
LanguageGHC2021

Rerefined.Predicate.Logical.Iff

Synopsis
  • data Iff (l :: k) (r :: k1)

Documentation

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