Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Documentation
data CompareValue op (sign :: Sign) (n :: Natural) Source #
Compare value to a type-level Natural
using the given RelOp
.
Instances
Predicate (CompareValue op sign n :: Type) Source # | Precedence of 4 (matching base relational operators e.g. |
Defined in Rerefined.Predicate.Relational.Value type PredicateName d (CompareValue op sign n) :: Symbol Source # | |
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => Refine (CompareValue op sign n :: Type) a Source # | |
Defined in Rerefined.Predicate.Relational.Value validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure Source # | |
type PredicateName d (CompareValue op sign n :: Type) Source # | |
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) |
data CompareLength op (n :: Natural) Source #
Compare length to a type-level Natural
using the given RelOp
.