Safe Haskell	None
Language	GHC2021

Rerefined.Predicate.Relational

Synopsis

Documentation

data CompareValue (op :: k) (sign :: Sign) (n :: Natural) Source #

Compare value to a type-level Natural using the given RelOp.

Instances details

Predicate (CompareValue op sign n :: Type) Source #	Precedence of 4 (matching base relational operators e.g. `>=`).
Instance details Defined in Rerefined.Predicate.Relational.Value
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => Refine (CompareValue op sign n :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure Source #
type PredicateName d (CompareValue op sign n :: Type) Source #
Instance details Defined in Rerefined.Predicate.Relational.Value type PredicateName d (CompareValue op sign n :: Type) = ShowParen (d > 4) (((("Value " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowSign sign) ++ ShowNatDec n)

Constructors

Pos
Neg

Compare length to a type-level Natural using the given RelOp.

Instances details

(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source #	Compare the length of a `Foldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source #
Predicate (CompareLength op n :: Type) Source #	Precedence of 4 (matching base relational operators e.g. `>=`).
Instance details Defined in Rerefined.Predicate.Relational.Length
(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a Source #	Compare the length of a `MonoFoldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure Source #
type PredicateName d (CompareLength op n :: Type) Source #
Instance details Defined in Rerefined.Predicate.Relational.Length type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)