Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Documentation
data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural) Source #
Instances
(Typeable op, Typeable sign, KnownNat n) => Predicate (CompareValue op sign n :: Type) Source # | |
Defined in Rerefined.Predicate.Relational.Value predicateName :: Proxy# (CompareValue op sign n) -> Int -> ShowS Source # | |
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, ReifySign sign) => Refine (CompareValue op sign n :: Type) a Source # | |
Defined in Rerefined.Predicate.Relational.Value validate :: Proxy# (CompareValue op sign n) -> a -> Maybe (RefineFailure String) Source # |
Relational operator.
There are three possible outcomes from compare
ing two terms, defined in
Ordering
. However, we may instead compare terms using relational operators
such as >=
, which are more specific comparisons that return a Bool
.
Constructor order is arbitrary due to NEQ
, which obstructs ordering in a
meaningful way.
data CompareLength (op :: RelOp) (n :: Natural) Source #
Instances
(KnownNat n, Foldable f, ReifyRelOp op) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe (RefineFailure String) Source # | |
(Typeable op, KnownNat n) => Predicate (CompareLength op n :: Type) Source # | |
Defined in Rerefined.Predicate.Relational.Length predicateName :: Proxy# (CompareLength op n) -> Int -> ShowS Source # | |
(KnownNat n, MonoFoldable a, ReifyRelOp op) => Refine (CompareLength op n :: Type) a Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length validate :: Proxy# (CompareLength op n) -> a -> Maybe (RefineFailure String) Source # |