Rerefined.Predicate.Logical.If

Documentation

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